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