let X, Y be set ; :: thesis: for f being Function st <:f,X,Y:> is total holds
X c= dom f
let f be Function; :: thesis: ( <:f,X,Y:> is total implies X c= dom f )
assume A1: dom <:f,X,Y:> = X ; :: according to PARTFUN1:def 2 :: thesis: X c= dom f
A2: dom <:f,X,Y:> c= dom f by Th77;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in dom f )
assume x in X ; :: thesis: x in dom f
hence x in dom f by A1, A2; :: thesis: verum