let x, 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 x in dom <:f,X,Y:> ; :: thesis: <:f,X,Y:> . x = f . x
then ( x in dom f & x in X & f . x in Y ) by Th78;
hence <:f,X,Y:> . x = f . x by Th79; :: thesis: verum