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 2;
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 Th7;
then (doms (A ?. o)) . i = dom (Den (o,(A . i))) by A1, FUNCT_6:22;
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 A1, FUNCT_6:def 2; :: thesis: verum