let ND be non empty set ; 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; ( <*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 )
by Th77;
A4:
( <*y1,y2,y3,y4,y5*> . 2 = y2 & <*y1,y2,y3,y4,y5*> . 3 = y3 )
by Th77;
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 Th77, 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; verum