let A, B, x be set ; :: thesis: for f being Function st x in A & f in Funcs (A,B) holds

f . x in B

let f be Function; :: thesis: ( x in A & f in Funcs (A,B) implies f . x in B )

assume A1: x in A ; :: thesis: ( not f in Funcs (A,B) or f . x in B )

assume A2: f in Funcs (A,B) ; :: thesis: f . x in B

then A3: f is Function of A,B by FUNCT_2:66;

( B = {} implies A = {} ) by A2;

hence f . x in B by A1, A3, FUNCT_2:5; :: thesis: verum

f . x in B

let f be Function; :: thesis: ( x in A & f in Funcs (A,B) implies f . x in B )

assume A1: x in A ; :: thesis: ( not f in Funcs (A,B) or f . x in B )

assume A2: f in Funcs (A,B) ; :: thesis: f . x in B

then A3: f is Function of A,B by FUNCT_2:66;

( B = {} implies A = {} ) by A2;

hence f . x in B by A1, A3, FUNCT_2:5; :: thesis: verum