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 Th14;
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:56; :: thesis: verum