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 A3: ( p . 1 = f1 . t1 & q . 1 = g1 . t2 ) by Th34;
A4: ( p . 2 = f2 . t1 & q . 2 = g2 . t2 ) by A1, Th34;
( p . 3 = f3 . t1 & q . 3 = g3 . t2 ) by A1, Th34;
hence ( f1 . t1 = g1 . t2 & f2 . t1 = g2 . t2 & f3 . t1 = g3 . t2 ) by A1, A3, A4; :: thesis: verum