let x be object ; :: thesis: for X, Y being set
for f being Function st x in dom <:f,X,Y:> holds
<:f,X,Y:> . x = f . x
let X, Y be set ; :: thesis: for f being Function st x in dom <:f,X,Y:> holds
<:f,X,Y:> . x = f . x
let f be Function; :: thesis: ( x in dom <:f,X,Y:> implies <:f,X,Y:> . x = f . x )
assume A1: x in dom <:f,X,Y:> ; :: thesis: <:f,X,Y:> . x = f . x
then ( x in dom f & f . x in Y ) by Th24;
hence <:f,X,Y:> . x = f . x by A1, Th25; :: thesis: verum