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