let X, Y be set ; :: thesis: for f being Function st X c= dom f & rng f c= Y holds
<:f,X,Y:> is total
let f be Function; :: thesis: ( X c= dom f & rng f c= Y implies <:f,X,Y:> is total )
assume that
A1: X c= dom f and
A2: rng f c= Y ; :: thesis: <:f,X,Y:> is total
X c= dom <:f,X,Y:>
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in dom <:f,X,Y:> )
assume A3: x in X ; :: thesis: x in dom <:f,X,Y:>
then f . x in rng f by A1, FUNCT_1:def 3;
hence x in dom <:f,X,Y:> by A1, A2, A3, Th24; :: thesis: verum
end;
hence dom <:f,X,Y:> = X ; :: according to PARTFUN1:def 2 :: thesis: verum