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 A1: ( not C = {} or B = {} or A = {} ) ; :: thesis: for f being Function of A,(Funcs B,C) holds rng (Frege f) c= Funcs A,C
let f be Function of A,(Funcs B,C); :: thesis: rng (Frege f) c= Funcs A,C
A2: ( Funcs B,C = {} implies A = {} ) by A1, FUNCT_2:11;
A3: SubFuncs (rng f) = rng f by Th4;
then A4: dom (rngs f) = f " (rng f) by FUNCT_6:def 3;
then A5: dom (rngs f) = dom f by RELAT_1:169
.= A by A2, FUNCT_2:def 1 ;
then A6: dom (rngs f) = dom (A --> C) by FUNCOP_1:19;
for x being set st x in dom (rngs f) holds
(rngs f) . x c= (A --> C) . x

proof

let x be set ; :: thesis: ( x in dom (rngs f) implies (rngs f) . x c= (A --> C) . x )
assume A7: x in dom (rngs f) ; :: thesis: (rngs f) . x c= (A --> C) . x
A8: f . x in Funcs B,C by A2, A5, A7, FUNCT_2:7;
(rngs f) . x = proj2 (f . x) by A3, A4, A7, FUNCT_6:def 3
.= rng (f . x) ;
then (rngs f) . x c= C by A8, FUNCT_2:169;
hence (rngs f) . x c= (A --> C) . x by A5, A7, FUNCOP_1:13; :: thesis: verum

end;

then product (rngs f) c= product (A --> C) by A6, CARD_3:38;
then product (rngs f) c= Funcs A,C by CARD_3:20;
hence rng (Frege f) c= Funcs A,C by FUNCT_6:58; :: thesis: verum