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 )
( <*f,g,h*> . 3 = h & 3 in Seg 3 & dom <*f,g,h*> = Seg 3 ) by ENUMSET1:def 1, FINSEQ_1:62, FINSEQ_3:1, FINSEQ_3:30;
hence ( x in dom h implies <*f,g,h*> .. 3,x = h . x ) by FUNCT_5:45; :: thesis: verum