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
for x being Element of Args o,(product A)
for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . 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
for x being Element of Args o,(product A)
for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . i
let A be MSAlgebra-Family of I,S; :: thesis: for i being Element of I
for o being OperSymbol of S
for x being Element of Args o,(product A)
for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . i
let i be Element of I; :: thesis: for o being OperSymbol of S
for x being Element of Args o,(product A)
for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . i
let o be OperSymbol of S; :: thesis: for x being Element of Args o,(product A)
for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . i
let x be Element of Args o,(product A); :: thesis: for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . i
let n be set ; :: thesis: ( n in dom (the_arity_of o) implies for f being Function st f = x . n holds
((commute x) . i) . n = f . i )
assume A1: n in dom (the_arity_of o) ; :: thesis: for f being Function st f = x . n holds
((commute x) . i) . n = f . i
set C = union { (the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ;
A2: x in Funcs (dom (the_arity_of o)),(Funcs I,(union { (the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) by Th15;
let g be Function; :: thesis: ( g = x . n implies ((commute x) . i) . n = g . i )
assume g = x . n ; :: thesis: ((commute x) . i) . n = g . i
hence ((commute x) . i) . n = g . i by A1, A2, FUNCT_6:86; :: thesis: verum