let D be non empty set ; :: thesis: for p1, p2, p3 being Element of D holds <*p1,p2,p3*> /^ 1 = <*p2,p3*>
let p1, p2, p3 be Element of D; :: thesis: <*p1,p2,p3*> /^ 1 = <*p2,p3*>
<*p1,p2,p3*> = <*p1*> ^ <*p2,p3*> by FINSEQ_1:60;
hence <*p1,p2,p3*> /^ 1 = <*p2,p3*> by Th49; :: thesis: verum