let I be non empty set ; :: thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st f in rng (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) )
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st f in rng (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) )
let A be MSAlgebra-Family of I,S; :: thesis: for o being OperSymbol of S
for f being Function st f in rng (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) )
let o be OperSymbol of S; :: thesis: for f being Function st f in rng (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) )
let f be Function; :: thesis: ( f in rng (Frege (A ?. o)) implies ( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) ) )
A1: dom (A ?. o) = I by PARTFUN1:def 2;
assume f in rng (Frege (A ?. o)) ; :: thesis: ( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) )
then consider y being object such that
A2: y in dom (Frege (A ?. o)) and
A3: (Frege (A ?. o)) . y = f by FUNCT_1:def 3;
A4: dom (Frege (A ?. o)) = product (doms (A ?. o)) by PARTFUN1:def 2;
then consider g being Function such that
A5: g = y and
a5: dom g = dom (doms (A ?. o)) and
A6: for i being object st i in dom (doms (A ?. o)) holds
g . i in (doms (A ?. o)) . i by A2, CARD_3:def 5;
ab: dom (doms (A ?. o)) = dom (A ?. o) by FUNCT_6:def 2
.= I by PARTFUN1:def 2 ;
A7: f = (A ?. o) .. g by A2, A3, A4, A5, Def2;
then dom f = (dom (A ?. o)) /\ (dom g) by PRALG_1:def 19;
hence a8: dom f = I /\ (dom g) by PARTFUN1:def 2
.= I by ab, a5 ;
:: thesis: for i being Element of I holds f . i in Result (o,(A . i))
let i be Element of I; :: thesis: f . i in Result (o,(A . i))
A8: (A ?. o) . i = Den (o,(A . i)) by Th7;
dom (doms (A ?. o)) = dom (A ?. o) by FUNCT_6:def 2;
then g . i in (doms (A ?. o)) . i by A6, A1;
then A9: g . i in dom (Den (o,(A . i))) by A1, A8, FUNCT_6:22;
f . i = (Den (o,(A . i))) . (g . i) by a8, A7, A8, PRALG_1:def 19;
then A10: f . i in rng (Den (o,(A . i))) by A9, FUNCT_1:def 3;
rng (Den (o,(A . i))) c= Result (o,(A . i)) by RELAT_1:def 19;
hence f . i in Result (o,(A . i)) by A10; :: thesis: verum