let X be set ; :: thesis: for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is onto holds
(f .: A) ` c= f .: (A `)
let Y be non empty set ; :: thesis: for f being Function of X,Y
for A being Subset of X st f is onto holds
(f .: A) ` c= f .: (A `)
let f be Function of X,Y; :: thesis: for A being Subset of X st f is onto holds
(f .: A) ` c= f .: (A `)
let A be Subset of X; :: thesis: ( f is onto implies (f .: A) ` c= f .: (A `) )
assume A1: f is onto ; :: thesis: (f .: A) ` c= f .: (A `)
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in (f .: A) ` or e in f .: (A `) )
assume A2: e in (f .: A) ` ; :: thesis: e in f .: (A `)
then reconsider y = e as Element of Y ;
consider u being object such that
A3: u in X and
A4: y = f . u by A1, Th1;
reconsider x = u as Element of X by A3;

now :: thesis: not x in A

assume x in A ; :: thesis: contradiction
then y in f .: A by A4, FUNCT_2:35;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum

end;

then x in A ` by A3, SUBSET_1:29;
hence e in f .: (A `) by A4, FUNCT_2:35; :: thesis: verum