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