let X, Y be non empty set ; :: thesis: for f being Function of X,Y
for A being Element of Fin X st f .: A = {} holds
A = {}
let f be Function of X,Y; :: thesis: for A being Element of Fin X st f .: A = {} holds
A = {}
let A be Element of Fin X; :: thesis: ( f .: A = {} implies A = {} )
assume A1: f .: A = {} ; :: thesis: A = {}
assume A <> {} ; :: thesis: contradiction
then consider x being Element of X such that
A2: x in A by Th9;
f . x in f .: A by A2, FUNCT_2:35;
hence contradiction by A1; :: thesis: verum