let f1, f2, f3 be PartFunc of REAL ,REAL ; :: thesis: for t being Real holds (VFunc f1,f2,f3) . t = (((f1 . t) * <e1> ) + ((f2 . t) * <e2> )) + ((f3 . t) * <e3> )
let t be Real; :: thesis: (VFunc f1,f2,f3) . t = (((f1 . t) * <e1> ) + ((f2 . t) * <e2> )) + ((f3 . t) * <e3> )
A2: ( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 ) by FINSEQ_1:62;
A3: ( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 ) by FINSEQ_1:62;
A4: ( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 ) by FINSEQ_1:62;
A5: (((f1 . t) * <e1> ) + ((f2 . t) * <e2> )) + ((f3 . t) * <e3> ) = (|[((f1 . t) * 1),((f1 . t) * 0 ),((f1 . t) * 0 )]| + ((f2 . t) * <e2> )) + ((f3 . t) * <e3> ) by A2, Lm3
.= (|[(f1 . t),0 ,0 ]| + |[((f2 . t) * 0 ),((f2 . t) * 1),((f2 . t) * 0 )]|) + ((f3 . t) * <e3> ) by A3, Lm3
.= (|[(f1 . t),0 ,0 ]| + |[0 ,(f2 . t),0 ]|) + |[((f3 . t) * 0 ),((f3 . t) * 0 ),((f3 . t) * 1)]| by A4, Lm3
.= (|[(f1 . t),0 ,0 ]| + |[0 ,(f2 . t),0 ]|) + |[0 ,0 ,(f3 . t)]| ;
A6: ( |[(f1 . t),0 ,0 ]| . 1 = f1 . t & |[(f1 . t),0 ,0 ]| . 2 = 0 & |[(f1 . t),0 ,0 ]| . 3 = 0 ) by FINSEQ_1:62;
A7: ( |[0 ,(f2 . t),0 ]| . 1 = 0 & |[0 ,(f2 . t),0 ]| . 2 = f2 . t & |[0 ,(f2 . t),0 ]| . 3 = 0 ) by FINSEQ_1:62;
A8: ( |[0 ,0 ,(f3 . t)]| . 1 = 0 & |[0 ,0 ,(f3 . t)]| . 2 = 0 & |[0 ,0 ,(f3 . t)]| . 3 = f3 . t ) by FINSEQ_1:62;
A9: (((f1 . t) * <e1> ) + ((f2 . t) * <e2> )) + ((f3 . t) * <e3> ) = |[((f1 . t) + 0 ),(0 + (f2 . t)),(0 + 0 )]| + |[0 ,0 ,(f3 . t)]| by A5, A6, A7, Lm4
.= |[(f1 . t),(f2 . t),0 ]| + |[0 ,0 ,(f3 . t)]| ;
( |[(f1 . t),(f2 . t),0 ]| . 1 = f1 . t & |[(f1 . t),(f2 . t),0 ]| . 2 = f2 . t & |[(f1 . t),(f2 . t),0 ]| . 3 = 0 ) by FINSEQ_1:62;
then (((f1 . t) * <e1> ) + ((f2 . t) * <e2> )) + ((f3 . t) * <e3> ) = |[((f1 . t) + 0 ),((f2 . t) + 0 ),(0 + (f3 . t))]| by A8, A9, Lm4
.= |[(f1 . t),(f2 . t),(f3 . t)]| ;
hence (VFunc f1,f2,f3) . t = (((f1 . t) * <e1> ) + ((f2 . t) * <e2> )) + ((f3 . t) * <e3> ) by Def1; :: thesis: verum