let X, Y be set ; :: thesis: for f being Function st dom f c= X & rng f c= Y holds
f = <:f,X,Y:>
let f be Function; :: thesis: ( dom f c= X & rng f c= Y implies f = <:f,X,Y:> )
assume that
A1: dom f c= X and
A2: rng f c= Y ; :: thesis: f = <:f,X,Y:>
A3: dom f c= dom <:f,X,Y:>

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in dom <:f,X,Y:> )
assume A4: x in dom f ; :: thesis: x in dom <:f,X,Y:>
then f . x in rng f by FUNCT_1:def 5;
hence x in dom <:f,X,Y:> by A1, A2, A4, Th78; :: thesis: verum

end;

dom <:f,X,Y:> c= dom f by Th77;
then A5: dom f = dom <:f,X,Y:> by A3, XBOOLE_0:def 10;
for x being set st x in dom f holds
f . x = <:f,X,Y:> . x by A3, Th80;
hence f = <:f,X,Y:> by A5, FUNCT_1:9; :: thesis: verum