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};
( dom <*y1,y2,y3,y4,y5*> = {1,2,3,4,5} & <*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 & 1 in {1,2,3,4,5} & 2 in {1,2,3,4,5} & 3 in {1,2,3,4,5} & 4 in {1,2,3,4,5} & 5 in {1,2,3,4,5} ) by Th93, Th94, 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 PARTFUN1:def 8; :: thesis: verum