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