let x be object ; :: thesis: 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; :: thesis: ( 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;
hence ( x in dom h implies <*f,g,h*> .. (3,x) = h . x ) by A1, FUNCT_5:38; :: thesis: verum