let D be non empty set ; :: thesis: for d1, d2, d3 being Element of D holds
( <*d1,d2,d3*> /. 1 = d1 & <*d1,d2,d3*> /. 2 = d2 & <*d1,d2,d3*> /. 3 = d3 )
let d1, d2, d3 be Element of D; :: thesis: ( <*d1,d2,d3*> /. 1 = d1 & <*d1,d2,d3*> /. 2 = d2 & <*d1,d2,d3*> /. 3 = d3 )
set s = <*d1,d2,d3*>;
A1: ( <*d1,d2,d3*> . 2 = d2 & <*d1,d2,d3*> . 3 = d3 ) by FINSEQ_1:45;
A2: ( 1 in {1,2,3} & 2 in {1,2,3} ) by FINSEQ_3:1;
A3: 3 in {1,2,3} by FINSEQ_3:1;
( dom <*d1,d2,d3*> = {1,2,3} & <*d1,d2,d3*> . 1 = d1 ) by FINSEQ_1:45, FINSEQ_1:89, FINSEQ_3:1;
hence ( <*d1,d2,d3*> /. 1 = d1 & <*d1,d2,d3*> /. 2 = d2 & <*d1,d2,d3*> /. 3 = d3 ) by A1, A2, A3, PARTFUN1:def 6; :: thesis: verum