let p, q be Element of REAL 3; :: thesis: for f1, f2, f3, g1, g2, g3 being PartFunc of REAL,REAL
for t1, t2 being Real st p = (VFunc (f1,f2,f3)) . t1 & q = (VFunc (g1,g2,g3)) . t2 & p = q holds
( f1 . t1 = g1 . t2 & f2 . t1 = g2 . t2 & f3 . t1 = g3 . t2 )
let f1, f2, f3, g1, g2, g3 be PartFunc of REAL,REAL; :: thesis: for t1, t2 being Real st p = (VFunc (f1,f2,f3)) . t1 & q = (VFunc (g1,g2,g3)) . t2 & p = q holds
( f1 . t1 = g1 . t2 & f2 . t1 = g2 . t2 & f3 . t1 = g3 . t2 )
let t1, t2 be Real; :: thesis: ( p = (VFunc (f1,f2,f3)) . t1 & q = (VFunc (g1,g2,g3)) . t2 & p = q implies ( f1 . t1 = g1 . t2 & f2 . t1 = g2 . t2 & f3 . t1 = g3 . t2 ) )
assume A1: ( p = (VFunc (f1,f2,f3)) . t1 & q = (VFunc (g1,g2,g3)) . t2 & p = q ) ; :: thesis: ( f1 . t1 = g1 . t2 & f2 . t1 = g2 . t2 & f3 . t1 = g3 . t2 )
then A2: ( p . 1 = f1 . t1 & q . 1 = g1 . t2 ) by Th41;
A3: ( p . 2 = f2 . t1 & q . 2 = g2 . t2 ) by A1, Th41;
( p . 3 = f3 . t1 & q . 3 = g3 . t2 ) by A1, Th41;
hence ( f1 . t1 = g1 . t2 & f2 . t1 = g2 . t2 & f3 . t1 = g3 . t2 ) by A1, A2, A3; :: thesis: verum