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