The Implement Of Fuanctional And Dual Space Of Linear Space In Mizar

Currently, with the development of computer technology, mechanical proving has become an active researching area. People create various machine languages program successfully based on mechanized method, and implement some mathematical problems's proving on computer. In Europe,the most commonly used machine language system is Mizar language system,which has the most scholars, the most extensively used and the greatest size of database.This paper describes the history and development of Mizar system and mechanical proving,and indicates how to write mathematics articles and conducts automatic inspection in Mizar system.The author gives some definitions and basic properties of functional of the linear space based on Mizar laguage, implements the definition and some properties of dual space.The author's main work as follows: 1. defines some definitions of functional of the linear space based on Mizar laguage,such as add, subtract, multiply and so on,implement some properties of functional operation;2. defines modal shift between linear space and vector space,implement the definition of linear space's dual space by the modal shift and the definition of vector space's dual space,and prove some properties and four conditions which the dual space should satisfy in the form of the theorem.All the above results are verified to be correct and the corresponding calculation methods and strict proofs are given in Mizar system.