let D be non empty set ; :: thesis: for d1, d2 being Element of D holds
( <*d1,d2*> /. 1 = d1 & <*d1,d2*> /. 2 = d2 )
let d1, d2 be Element of D; :: thesis: ( <*d1,d2*> /. 1 = d1 & <*d1,d2*> /. 2 = d2 )
set s = <*d1,d2*>;
( dom <*d1,d2*> = {1,2} & <*d1,d2*> . 1 = d1 & <*d1,d2*> . 2 = d2 & 1 in {1,2} & 2 in {1,2} ) by FINSEQ_1:4, FINSEQ_1:61, FINSEQ_3:29;
hence ( <*d1,d2*> /. 1 = d1 & <*d1,d2*> /. 2 = d2 ) by PARTFUN1:def 8; :: thesis: verum