let I be non empty set ; 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 ; 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; 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; 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; ( 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 <> {}
; 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; 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)); (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; verum