let X, Y be non empty set ; :: thesis: for A being Element of Fin X
for B being set
for f being Function of X,Y st ( for x being Element of X st x in A holds
f . x in B ) holds
f .: A c= B
let A be Element of Fin X; :: thesis: for B being set
for f being Function of X,Y st ( for x being Element of X st x in A holds
f . x in B ) holds
f .: A c= B
let B be set ; :: thesis: for f being Function of X,Y st ( for x being Element of X st x in A holds
f . x in B ) holds
f .: A c= B
let f be Function of X,Y; :: thesis: ( ( for x being Element of X st x in A holds
f . x in B ) implies f .: A c= B )
assume A1: for x being Element of X st x in A holds
f . x in B ; :: thesis: f .: A c= B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: A or x in B )
assume x in f .: A ; :: thesis: x in B
then consider y being object such that
y in dom f and
A2: y in A and
A3: x = f . y by FUNCT_1:def 6;
reconsider y = y as Element of X by A2, Th6;
x = f . y by A3;
hence x in B by A1, A2; :: thesis: verum