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