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