let n be non empty Nat; :: thesis: for At being Subset of (TOP-REAL n)
for Ar being Subset of (n -VectSp_over F_Real) st At = Ar holds
( the carrier of (Lin At) = the carrier of (Lin Ar) & 0. (Lin At) = 0. (Lin Ar) & the addF of (Lin At) = the addF of (Lin Ar) & the Mult of (Lin At) = the lmult of (Lin Ar) )
let At be Subset of (TOP-REAL n); :: thesis: for Ar being Subset of (n -VectSp_over F_Real) st At = Ar holds
( the carrier of (Lin At) = the carrier of (Lin Ar) & 0. (Lin At) = 0. (Lin Ar) & the addF of (Lin At) = the addF of (Lin Ar) & the Mult of (Lin At) = the lmult of (Lin Ar) )
let Ar be Subset of (n -VectSp_over F_Real); :: thesis: ( At = Ar implies ( the carrier of (Lin At) = the carrier of (Lin Ar) & 0. (Lin At) = 0. (Lin Ar) & the addF of (Lin At) = the addF of (Lin Ar) & the Mult of (Lin At) = the lmult of (Lin Ar) ) )
assume A1: At = Ar ; :: thesis: ( the carrier of (Lin At) = the carrier of (Lin Ar) & 0. (Lin At) = 0. (Lin Ar) & the addF of (Lin At) = the addF of (Lin Ar) & the Mult of (Lin At) = the lmult of (Lin Ar) )
set V = TOP-REAL n;
set W = n -VectSp_over F_Real;
set Lt = Lin At;
set Lr = Lin Ar;
A2: ( the carrier of (Lin Ar) c= the carrier of (n -VectSp_over F_Real) & 0. (Lin Ar) = 0. (n -VectSp_over F_Real) & the addF of (Lin Ar) = the addF of (n -VectSp_over F_Real) || the carrier of (Lin Ar) & the lmult of (Lin Ar) = the lmult of (n -VectSp_over F_Real) | [: the carrier of F_Real, the carrier of (Lin Ar):] ) by VECTSP_4:def 2;
A3: ( the carrier of (Lin At) c= the carrier of (TOP-REAL n) & 0. (Lin At) = 0. (TOP-REAL n) & the addF of (Lin At) = the addF of (TOP-REAL n) || the carrier of (Lin At) & the Mult of (Lin At) = the Mult of (TOP-REAL n) | [:REAL, the carrier of (Lin At):] ) by RLSUB_1:def 2;
thus A4: the carrier of (Lin At) = [#] (Lin At)
.= [#] (Lin Ar) by A1, MATRTOP2:6
.= the carrier of (Lin Ar) ; :: thesis: ( 0. (Lin At) = 0. (Lin Ar) & the addF of (Lin At) = the addF of (Lin Ar) & the Mult of (Lin At) = the lmult of (Lin Ar) )
A5: the addF of (Lin At) = the addF of (n -VectSp_over F_Real) || the carrier of (Lin Ar) by A3, A4, Th54
.= the addF of (Lin Ar) by VECTSP_4:def 2 ;
the Mult of (Lin At) = the lmult of (n -VectSp_over F_Real) | [:REAL, the carrier of (Lin Ar):] by A3, A4, Th54
.= the lmult of (Lin Ar) by VECTSP_4:def 2 ;
hence ( 0. (Lin At) = 0. (Lin Ar) & the addF of (Lin At) = the addF of (Lin Ar) & the Mult of (Lin At) = the lmult of (Lin Ar) ) by A2, A3, A5, Th54; :: thesis: verum