let X, Y be set ; :: thesis: for f being Function st <:f,X,Y:> is total holds
f .: X c= Y
let f be Function; :: thesis: ( <:f,X,Y:> is total implies f .: X c= Y )
assume A1: dom <:f,X,Y:> = X ; :: according to PARTFUN1:def 2 :: thesis: f .: X c= Y
let y be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum