let F be ManySortedFunction of product (doms f); :: thesis: ( F = Frege f iff for g being Function st g in product (doms f) holds
F . g = f .. g )
thus ( F = Frege f implies for g being Function st g in product (doms f) holds
F . g = f .. g ) :: thesis: ( ( for g being Function st g in product (doms f) holds
F . g = f .. g ) implies F = Frege f )
proof
assume A3: F = Frege f ; :: thesis: for g being Function st g in product (doms f) holds
F . g = f .. g
let g be Function; :: thesis: ( g in product (doms f) implies F . g = f .. g )
assume A4: g in product (doms f) ; :: thesis: F . g = f .. g
then consider h being Function such that
A5: F . g = h and
A6: dom h = dom f and
A7: for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) by A3, FUNCT_6:def 7;
consider gg being Function such that
a13: ( g = gg & dom gg = dom (doms f) & ( for y being object st y in dom (doms f) holds
gg . y in (doms f) . y ) ) by CARD_3:def 5, A4;
dom g = dom f by a13, FUNCT_6:def 2;
then A8: dom h = (dom f) /\ (dom g) by A6;
for x being set st x in dom h holds
h . x = (f . x) . (g . x)
proof
let x be set ; :: thesis: ( x in dom h implies h . x = (f . x) . (g . x) )
assume A9: x in dom h ; :: thesis: h . x = (f . x) . (g . x)
then x in dom (doms f) by A6, FUNCT_6:def 2;
then g . x in (doms f) . x by A4, CARD_3:9;
then A10: g . x in dom (f . x) by A9, A6, FUNCT_6:22;
thus h . x = f .. (x,(g . x)) by A7, A9
.= (f . x) . (g . x) by A9, A6, A10, FUNCT_5:38 ; :: thesis: verum
end;
hence F . g = f .. g by A5, A8, PRALG_1:def 19; :: thesis: verum
end;
assume A11: for g being Function st g in product (doms f) holds
F . g = f .. g ; :: thesis: F = Frege f
A12: for g being Function st g in product (doms f) holds
ex h being Function st
( F . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) )
proof
let g be Function; :: thesis: ( g in product (doms f) implies ex h being Function st
( F . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) ) )
assume A13: g in product (doms f) ; :: thesis: ex h being Function st
( F . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) )
consider gg being Function such that
a13: ( g = gg & dom gg = dom (doms f) & ( for y being object st y in dom (doms f) holds
gg . y in (doms f) . y ) ) by CARD_3:def 5, A13;
a14: F . g = f .. g by A11, A13;
then A14: dom (F . g) = (dom f) /\ (dom g) by PRALG_1:def 19;
take F . g ; :: thesis: ( F . g = F . g & dom (F . g) = dom f & ( for x being object st x in dom (F . g) holds
(F . g) . x = (uncurry f) . (x,(g . x)) ) )
thus F . g = F . g ; :: thesis: ( dom (F . g) = dom f & ( for x being object st x in dom (F . g) holds
(F . g) . x = (uncurry f) . (x,(g . x)) ) )
WW: dom g = dom f by a13, FUNCT_6:def 2;
hence dom (F . g) = dom f by A14; :: thesis: for x being object st x in dom (F . g) holds
(F . g) . x = (uncurry f) . (x,(g . x))
let x be object ; :: thesis: ( x in dom (F . g) implies (F . g) . x = (uncurry f) . (x,(g . x)) )
assume A15: x in dom (F . g) ; :: thesis: (F . g) . x = (uncurry f) . (x,(g . x))
then x in dom (doms f) by WW, A14, FUNCT_6:def 2;
then g . x in (doms f) . x by A13, CARD_3:9;
then A16: g . x in dom (f . x) by A14, A15, FUNCT_6:22, WW;
thus (F . g) . x = (f .. g) . x by A11, A13
.= (f . x) . (g . x) by A15, PRALG_1:def 19, a14
.= (uncurry f) . (x,(g . x)) by A14, A15, A16, FUNCT_5:38, WW ; :: thesis: verum
end;
dom F = product (doms f) by PARTFUN1:def 2;
hence F = Frege f by A12, FUNCT_6:def 7; :: thesis: verum