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>)
A1: ( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 ) ;
A2: ( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 ) ;
A3: ( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 ) ;
A4: (((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 A1, Lm1
.= (|[(f1 . t),0,0]| + |[((f2 . t) * 0),((f2 . t) * 1),((f2 . t) * 0)]|) + ((f3 . t) * <e3>) by A2, Lm1
.= (|[(f1 . t),0,0]| + |[0,(f2 . t),0]|) + |[((f3 . t) * 0),((f3 . t) * 0),((f3 . t) * 1)]| by A3, Lm1
.= (|[(f1 . t),0,0]| + |[0,(f2 . t),0]|) + |[0,0,(f3 . t)]| ;
A5: ( |[(f1 . t),0,0]| . 1 = f1 . t & |[(f1 . t),0,0]| . 2 = 0 & |[(f1 . t),0,0]| . 3 = 0 ) ;
A6: ( |[0,(f2 . t),0]| . 1 = 0 & |[0,(f2 . t),0]| . 2 = f2 . t & |[0,(f2 . t),0]| . 3 = 0 ) ;
A7: ( |[0,0,(f3 . t)]| . 1 = 0 & |[0,0,(f3 . t)]| . 2 = 0 & |[0,0,(f3 . t)]| . 3 = f3 . t ) ;
A8: (((f1 . t) * <e1>) + ((f2 . t) * <e2>)) + ((f3 . t) * <e3>) = |[((f1 . t) + 0),(0 + (f2 . t)),(0 + 0)]| + |[0,0,(f3 . t)]| by A4, A5, A6, Lm2
.= |[(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 ) ;
then (((f1 . t) * <e1>) + ((f2 . t) * <e2>)) + ((f3 . t) * <e3>) = |[((f1 . t) + 0),((f2 . t) + 0),(0 + (f3 . t))]| by A7, A8, Lm2
.= |[(f1 . t),(f2 . t),(f3 . t)]| ;
hence (VFunc (f1,f2,f3)) . t = (((f1 . t) * <e1>) + ((f2 . t) * <e2>)) + ((f3 . t) * <e3>) by Def5; :: thesis: verum