let X, Y be set ; for f being Function st <:f,X,Y:> is total holds
f .: X c= Y
let f be Function; ( <:f,X,Y:> is total implies f .: X c= Y )
assume A1:
dom <:f,X,Y:> = X
; PARTFUN1:def 2 f .: X c= Y
let y be object ; TARSKI:def 3 ( not y in f .: X or y in Y )
A2:
rng <:f,X,Y:> c= Y
by RELAT_1:def 19;
assume
y in f .: X
; y in Y
then consider x being object such that
x in dom f
and
A3:
( x in X & y = f . x )
by FUNCT_1:def 6;
( <:f,X,Y:> . x = y & <:f,X,Y:> . x in rng <:f,X,Y:> )
by A1, A3, Th26, FUNCT_1:def 3;
hence
y in Y
by A2; verum