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 of 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 of 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 of 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 of 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 of 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 of 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 of 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:18;
commute x in product (doms (A ?. o)) by A1, Th18;
then (commute x) . i in (doms (A ?. o)) . i by A2, CARD_3:18;
hence (commute x) . i is Element of Args o,(A . i) by PRALG_2:18; :: thesis: verum