let p1, p2, q be Element of REAL 3; :: thesis: for f1, f2, f3, g1, g2, g3 being PartFunc of ,
for t1, t2, t being Real st p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t holds
|{p1,p2,q}| = |((q <X> p1),p2)|
let f1, f2, f3, g1, g2, g3 be PartFunc of ,; :: thesis: for t1, t2, t being Real st p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t holds
|{p1,p2,q}| = |((q <X> p1),p2)|
let t1, t2, t be Real; :: thesis: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t implies |{p1,p2,q}| = |((q <X> p1),p2)| )
assume A1: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t ) ; :: thesis: |{p1,p2,q}| = |((q <X> p1),p2)|
|{p1,p2,q}| = |{p2,q,p1}| by A1, ThA52;
hence |{p1,p2,q}| = |((q <X> p1),p2)| ; :: thesis: verum