let A, B, C be set ; :: thesis: ( ( not C = {} or B = {} or A = {} ) implies for f being Function of A,(Funcs (B,C)) holds rng (Frege f) c= Funcs (A,C) )

assume ( not C = {} or B = {} or A = {} ) ; :: thesis: for f being Function of A,(Funcs (B,C)) holds rng (Frege f) c= Funcs (A,C)

then A1: ( Funcs (B,C) = {} implies A = {} ) by FUNCT_2:8;

let f be Function of A,(Funcs (B,C)); :: thesis: rng (Frege f) c= Funcs (A,C)

A2: dom (rngs f) = dom f by FUNCT_6:def 3;

then A3: dom (rngs f) = A by A1, FUNCT_2:def 1;

A4: for x being object st x in dom (rngs f) holds

(rngs f) . x c= (A --> C) . x

then product (rngs f) c= product (A --> C) by A4, CARD_3:27;

then product (rngs f) c= Funcs (A,C) by CARD_3:11;

hence rng (Frege f) c= Funcs (A,C) by FUNCT_6:38; :: thesis: verum

assume ( not C = {} or B = {} or A = {} ) ; :: thesis: for f being Function of A,(Funcs (B,C)) holds rng (Frege f) c= Funcs (A,C)

then A1: ( Funcs (B,C) = {} implies A = {} ) by FUNCT_2:8;

let f be Function of A,(Funcs (B,C)); :: thesis: rng (Frege f) c= Funcs (A,C)

A2: dom (rngs f) = dom f by FUNCT_6:def 3;

then A3: dom (rngs f) = A by A1, FUNCT_2:def 1;

A4: for x being object st x in dom (rngs f) holds

(rngs f) . x c= (A --> C) . x

proof

dom (rngs f) = dom (A --> C)
by A3;
let x be object ; :: thesis: ( x in dom (rngs f) implies (rngs f) . x c= (A --> C) . x )

assume A5: x in dom (rngs f) ; :: thesis: (rngs f) . x c= (A --> C) . x

A6: (rngs f) . x = rng (f . x) by A2, A5, FUNCT_6:def 3;

f . x in Funcs (B,C) by A1, A3, A5, FUNCT_2:5;

then (rngs f) . x c= C by A6, FUNCT_2:92;

hence (rngs f) . x c= (A --> C) . x by A3, A5, FUNCOP_1:7; :: thesis: verum

end;assume A5: x in dom (rngs f) ; :: thesis: (rngs f) . x c= (A --> C) . x

A6: (rngs f) . x = rng (f . x) by A2, A5, FUNCT_6:def 3;

f . x in Funcs (B,C) by A1, A3, A5, FUNCT_2:5;

then (rngs f) . x c= C by A6, FUNCT_2:92;

hence (rngs f) . x c= (A --> C) . x by A3, A5, FUNCOP_1:7; :: thesis: verum

then product (rngs f) c= product (A --> C) by A4, CARD_3:27;

then product (rngs f) c= Funcs (A,C) by CARD_3:11;

hence rng (Frege f) c= Funcs (A,C) by FUNCT_6:38; :: thesis: verum