let ND be non empty set ; :: thesis: for y1, y2, y3, y4, y5 being Element of ND holds
( <*y1,y2,y3,y4,y5*> /. 1 = y1 & <*y1,y2,y3,y4,y5*> /. 2 = y2 & <*y1,y2,y3,y4,y5*> /. 3 = y3 & <*y1,y2,y3,y4,y5*> /. 4 = y4 & <*y1,y2,y3,y4,y5*> /. 5 = y5 )
let y1, y2, y3, y4, y5 be Element of ND; :: thesis: ( <*y1,y2,y3,y4,y5*> /. 1 = y1 & <*y1,y2,y3,y4,y5*> /. 2 = y2 & <*y1,y2,y3,y4,y5*> /. 3 = y3 & <*y1,y2,y3,y4,y5*> /. 4 = y4 & <*y1,y2,y3,y4,y5*> /. 5 = y5 )
set s = <*y1,y2,y3,y4,y5*>;
set i5 = {1,2,3,4,5};
A1: ( 1 in {1,2,3,4,5} & 2 in {1,2,3,4,5} ) by FINSEQ_3:3;
A2: ( 3 in {1,2,3,4,5} & 4 in {1,2,3,4,5} ) by FINSEQ_3:3;
A3: ( <*y1,y2,y3,y4,y5*> . 4 = y4 & <*y1,y2,y3,y4,y5*> . 5 = y5 ) ;
A4: ( <*y1,y2,y3,y4,y5*> . 2 = y2 & <*y1,y2,y3,y4,y5*> . 3 = y3 ) ;
A5: 5 in {1,2,3,4,5} by FINSEQ_3:3;
( dom <*y1,y2,y3,y4,y5*> = {1,2,3,4,5} & <*y1,y2,y3,y4,y5*> . 1 = y1 ) by FINSEQ_1:89, FINSEQ_3:3;
hence ( <*y1,y2,y3,y4,y5*> /. 1 = y1 & <*y1,y2,y3,y4,y5*> /. 2 = y2 & <*y1,y2,y3,y4,y5*> /. 3 = y3 & <*y1,y2,y3,y4,y5*> /. 4 = y4 & <*y1,y2,y3,y4,y5*> /. 5 = y5 ) by A4, A3, A1, A2, A5, PARTFUN1:def 6; :: thesis: verum