let x be set ; :: thesis: for f, g, h being Function st x in dom f holds
( <*f*> .. (1,x) = f . x & <*f,g*> .. (1,x) = f . x & <*f,g,h*> .. (1,x) = f . x )
let f, g, h be Function; :: thesis: ( x in dom f implies ( <*f*> .. (1,x) = f . x & <*f,g*> .. (1,x) = f . x & <*f,g,h*> .. (1,x) = f . x ) )
A1: ( <*f,g,h*> . 1 = f & 1 in Seg 1 ) by FINSEQ_1:4, FINSEQ_1:62, TARSKI:def 1;
A2: ( dom <*f*> = Seg 1 & dom <*f,g*> = Seg 2 ) by FINSEQ_1:def 8, FINSEQ_3:29;
A3: ( 1 in Seg 2 & 1 in Seg 3 ) by ENUMSET1:def 1, FINSEQ_1:4, FINSEQ_3:1, TARSKI:def 2;
A4: dom <*f,g,h*> = Seg 3 by FINSEQ_3:30;
( <*f*> . 1 = f & <*f,g*> . 1 = f ) by FINSEQ_1:61, FINSEQ_1:def 8;
hence ( x in dom f implies ( <*f*> .. (1,x) = f . x & <*f,g*> .. (1,x) = f . x & <*f,g,h*> .. (1,x) = f . x ) ) by A1, A3, A2, A4, FUNCT_5:45; :: thesis: verum