let I be non empty set ; :: thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for i being Element of I
for o being OperSymbol of S st the_arity_of o <> {} holds
for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for i being Element of I
for o being OperSymbol of S st the_arity_of o <> {} holds
for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))
let A be MSAlgebra-Family of I,S; :: thesis: for i being Element of I
for o being OperSymbol of S st the_arity_of o <> {} holds
for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))
let i be Element of I; :: thesis: for o being OperSymbol of S st the_arity_of o <> {} holds
for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))
let o be OperSymbol of S; :: thesis: ( the_arity_of o <> {} implies for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i)) )
assume A1: the_arity_of o <> {} ; :: thesis: for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))
let U1 be non-empty MSAlgebra over S; :: thesis: for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))
let x be Element of Args (o,(product A)); :: thesis: (commute x) . i is Element of Args (o,(A . i))
i in I ;
then A2: i in dom (doms (A ?. o)) by PRALG_2:11;
commute x in product (doms (A ?. o)) by A1, Th17;
then (commute x) . i in (doms (A ?. o)) . i by A2, CARD_3:9;
hence (commute x) . i is Element of Args (o,(A . i)) by PRALG_2:11; :: thesis: verum