let X be set ; :: thesis: for f being Function holds
( dom (Frege (X --> f)) = Funcs (X,(dom f)) & rng (Frege (X --> f)) = Funcs (X,(rng f)) & ( for g being Function st g in Funcs (X,(dom f)) holds
(Frege (X --> f)) . g = f * g ) )
let f be Function; :: thesis: ( dom (Frege (X --> f)) = Funcs (X,(dom f)) & rng (Frege (X --> f)) = Funcs (X,(rng f)) & ( for g being Function st g in Funcs (X,(dom f)) holds
(Frege (X --> f)) . g = f * g ) )
A1: product (X --> (dom f)) = Funcs (X,(dom f)) by CARD_3:20;
A2: doms (X --> f) = X --> (dom f) by Th36;
( rngs (X --> f) = X --> (rng f) & product (X --> (rng f)) = Funcs (X,(rng f)) ) by Th36, CARD_3:20;
hence ( dom (Frege (X --> f)) = Funcs (X,(dom f)) & rng (Frege (X --> f)) = Funcs (X,(rng f)) ) by A2, A1, Def7, Th58; :: thesis: for g being Function st g in Funcs (X,(dom f)) holds
(Frege (X --> f)) . g = f * g
let g be Function; :: thesis: ( g in Funcs (X,(dom f)) implies (Frege (X --> f)) . g = f * g )
assume A3: g in Funcs (X,(dom f)) ; :: thesis: (Frege (X --> f)) . g = f * g
then consider h being Function such that
A4: (Frege (X --> f)) . g = h and
A5: dom h = (X --> f) " (SubFuncs (rng (X --> f))) and
A6: for x being set st x in dom h holds
h . x = (uncurry (X --> f)) . (x,(g . x)) by A2, A1, Def7;
dom (X --> (dom f)) = X by FUNCOP_1:19;
then A7: dom h = X by A2, A5, Def2;
A8: ex g9 being Function st
( g = g9 & dom g9 = X & rng g9 c= dom f ) by A3, FUNCT_2:def 2;
then A9: dom (f * g) = X by RELAT_1:46;
A10: dom (X --> f) = X by FUNCOP_1:19;

now

let x be set ; :: thesis: ( x in X implies (f * g) . x = h . x )
assume A11: x in X ; :: thesis: (f * g) . x = h . x
then A12: ( h . x = (uncurry (X --> f)) . (x,(g . x)) & (X --> f) . x = f ) by A6, A7, FUNCOP_1:13;
( g . x in rng g & (f * g) . x = f . (g . x) ) by A8, A9, A11, FUNCT_1:22, FUNCT_1:def 5;
hence (f * g) . x = h . x by A8, A10, A11, A12, FUNCT_5:45; :: thesis: verum

end;

hence (Frege (X --> f)) . g = f * g by A4, A7, A9, FUNCT_1:9; :: thesis: verum