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) ) ) )
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 set such that
A1: ( y in dom (Frege (A ?. o)) & (Frege (A ?. o)) . y = f ) by FUNCT_1:def 5;
A2: dom (Frege (A ?. o)) = product (doms (A ?. o)) by PARTFUN1:def 4;
then consider g being Function such that
A3: ( g = y & dom g = dom (doms (A ?. o)) & ( for i being set st i in dom (doms (A ?. o)) holds
g . i in (doms (A ?. o)) . i ) ) by A1, CARD_3:def 5;
A4: f = (A ?. o) .. g by A1, A2, A3, Def8;
hence dom f = dom (A ?. o) by PRALG_1:def 17
.= I by PARTFUN1:def 4 ;
:: thesis: for i being Element of I holds f . i in Result o,(A . i)
A5: dom (A ?. o) = I by PARTFUN1:def 4;
let i be Element of I; :: thesis: f . i in Result o,(A . i)
A6: (A ?. o) . i = Den o,(A . i) by Th14;
then A7: f . i = (Den o,(A . i)) . (g . i) by A4, A5, PRALG_1:def 17;
A8: SubFuncs (rng (A ?. o)) = rng (A ?. o)

proof

thus SubFuncs (rng (A ?. o)) c= rng (A ?. o) by FUNCT_6:27; :: according to XBOOLE_0:def 10 :: thesis: rng (A ?. o) c= SubFuncs (rng (A ?. o))
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (A ?. o) or x in SubFuncs (rng (A ?. o)) )
assume A9: x in rng (A ?. o) ; :: thesis: x in SubFuncs (rng (A ?. o))
then ex j being set st
( j in dom (A ?. o) & x = (A ?. o) . j ) by FUNCT_1:def 5;
hence x in SubFuncs (rng (A ?. o)) by A9, FUNCT_6:def 1; :: thesis: verum

end;

dom (doms (A ?. o)) = (A ?. o) " (SubFuncs (rng (A ?. o))) by FUNCT_6:def 2
.= dom (A ?. o) by A8, RELAT_1:169 ;
then g . i in (doms (A ?. o)) . i by A3, A5;
then g . i in dom (Den o,(A . i)) by A5, A6, FUNCT_6:31;
then ( f . i in rng (Den o,(A . i)) & rng (Den o,(A . i)) c= Result o,(A . i) ) by A7, FUNCT_1:def 5, RELAT_1:def 19;
hence f . i in Result o,(A . i) ; :: thesis: verum