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 4 :: thesis: f .: X c= Y
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: X or y in Y )
assume y in f .: X ; :: thesis: y in Y
then consider x being set such that
A2: ( x in dom f & x in X & y = f . x ) by FUNCT_1:def 12;
( <:f,X,Y:> . x = y & <:f,X,Y:> . x in rng <:f,X,Y:> & rng <:f,X,Y:> c= Y ) by A1, A2, Th80, FUNCT_1:def 5, RELAT_1:def 19;
hence y in Y ; :: thesis: verum