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 holds
( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args 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 holds
( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args o,(A . i) ) )
let A be MSAlgebra-Family of I,S; :: thesis: for o being OperSymbol of S holds
( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args o,(A . i) ) )
let o be OperSymbol of S; :: thesis: ( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args o,(A . i) ) )
A1: dom (A ?. o) = I by PARTFUN1:def 4;
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 A2: 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 A2, FUNCT_6:def 1; :: thesis: verum

end;

then A3: (A ?. o) " (SubFuncs (rng (A ?. o))) = dom (A ?. o) by RELAT_1:169
.= I by PARTFUN1:def 4 ;
for i being Element of I holds (doms (A ?. o)) . i = Args o,(A . i)

proof

let i be Element of I; :: thesis: (doms (A ?. o)) . i = Args o,(A . i)
(A ?. o) . i = Den o,(A . i) by Th14;
then (doms (A ?. o)) . i = dom (Den o,(A . i)) by A1, FUNCT_6:31;
hence (doms (A ?. o)) . i = Args o,(A . i) by FUNCT_2:def 1; :: thesis: verum

end;

hence ( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args o,(A . i) ) ) by A3, FUNCT_6:def 2; :: thesis: verum