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*>;
A1: ( <*d1,d2*> . 2 = d2 & 1 in {1,2} ) by FINSEQ_1:4, FINSEQ_1:61;
A2: 2 in {1,2} by FINSEQ_1:4;
( dom <*d1,d2*> = {1,2} & <*d1,d2*> . 1 = d1 ) by FINSEQ_1:4, FINSEQ_1:61, FINSEQ_3:29;
hence ( <*d1,d2*> /. 1 = d1 & <*d1,d2*> /. 2 = d2 ) by A1, A2, PARTFUN1:def 8; :: thesis: verum