let I be non empty set ; :: thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args o,(product A) st the_arity_of o <> {} holds
for i being Element of I holds (proj A,i) # x = (commute x) . i
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args o,(product A) st the_arity_of o <> {} holds
for i being Element of I holds (proj A,i) # x = (commute x) . i
let A be MSAlgebra-Family of I,S; :: thesis: for o being OperSymbol of S
for x being Element of Args o,(product A) st the_arity_of o <> {} holds
for i being Element of I holds (proj A,i) # x = (commute x) . i
let o be OperSymbol of S; :: thesis: for x being Element of Args o,(product A) st the_arity_of o <> {} holds
for i being Element of I holds (proj A,i) # x = (commute x) . i
let x be Element of Args o,(product A); :: thesis: ( the_arity_of o <> {} implies for i being Element of I holds (proj A,i) # x = (commute x) . i )
assume A1: the_arity_of o <> {} ; :: thesis: for i being Element of I holds (proj A,i) # x = (commute x) . 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 } ;
let i be Element of I; :: thesis: (proj A,i) # x = (commute x) . i
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;
then A3: commute x in Funcs I,(Funcs (dom (the_arity_of o)),(union { (the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) by A1, FUNCT_6:85;
then dom (commute x) = I by FUNCT_2:169;
then A4: (commute x) . i in rng (commute x) by FUNCT_1:def 5;

A5: now

A6: rng x c= 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 A2, FUNCT_2:169;
let n be set ; :: thesis: ( n in dom (the_arity_of o) implies ((proj A,i) # x) . n = ((commute x) . i) . n )
assume A7: n in dom (the_arity_of o) ; :: thesis: ((proj A,i) # x) . n = ((commute x) . i) . n
x . n in product (Carrier A,((the_arity_of o) /. n)) by A7, Th16;
then A8: x . n in dom (proj (Carrier A,((the_arity_of o) /. n)),i) by CARD_3:def 17;
n in dom x by A2, A7, FUNCT_2:169;
then x . n in rng x by FUNCT_1:def 5;
then consider g being Function such that
A9: g = x . n and
dom g = I and
rng g c= union { (the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } by A6, FUNCT_2:def 2;
thus ((proj A,i) # x) . n = ((proj A,i) . ((the_arity_of o) /. n)) . (x . n) by A7, Th14
.= (proj (Carrier A,((the_arity_of o) /. n)),i) . (x . n) by Def3
.= g . i by A9, A8, CARD_3:def 17
.= ((commute x) . i) . n by A2, A7, A9, FUNCT_6:86 ; :: thesis: verum

end;

A10: x in product (doms ((proj A,i) * (the_arity_of o))) by Th13;
rng (commute x) c= Funcs (dom (the_arity_of o)),(union { (the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ) by A3, FUNCT_2:169;
then A11: dom ((commute x) . i) = dom (the_arity_of o) by A4, FUNCT_2:169;
dom (proj A,i) = the carrier of S by PARTFUN1:def 4;
then A12: rng (the_arity_of o) c= dom (proj A,i) ;
dom ((proj A,i) # x) = dom ((Frege ((proj A,i) * (the_arity_of o))) . x) by MSUALG_3:def 7
.= dom (((proj A,i) * (the_arity_of o)) .. x) by A10, PRALG_2:def 8
.= dom ((proj A,i) * (the_arity_of o)) by PRALG_1:def 17
.= dom (the_arity_of o) by A12, RELAT_1:46 ;
hence (proj A,i) # x = (commute x) . i by A11, A5, FUNCT_1:9; :: thesis: verum