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 Th14;
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:55;
then dom (commute x) = I by FUNCT_2:92;
then A4: (commute x) . i in rng (commute x) by FUNCT_1:def 3;
SS: dom x = dom (the_arity_of o) by MSUALG_6:2;

A5: now :: thesis: for n being object st n in dom (the_arity_of o) holds
((proj (A,i)) # x) . n = ((commute x) . i) . n

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:92;
let n be object ; :: 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, Th15;
then A8: x . n in dom (proj ((Carrier (A,((the_arity_of o) /. n))),i)) by CARD_3:def 16;
n in dom x by A2, A7, FUNCT_2:92;
then x . n in rng x by FUNCT_1:def 3;
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, Th13
.= (proj ((Carrier (A,((the_arity_of o) /. n))),i)) . (x . n) by Def2
.= g . i by A9, A8, CARD_3:def 16
.= ((commute x) . i) . n by A2, A7, A9, FUNCT_6:56 ; :: thesis: verum

end;

A10: x in product (doms ((proj (A,i)) * (the_arity_of o))) by Th12;
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:92;
then A11: dom ((commute x) . i) = dom (the_arity_of o) by A4, FUNCT_2:92;
dom (proj (A,i)) = the carrier of S by PARTFUN1:def 2;
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 5
.= dom (((proj (A,i)) * (the_arity_of o)) .. x) by A10, PRALG_2:def 2
.= (dom ((proj (A,i)) * (the_arity_of o))) /\ (dom x) by PRALG_1:def 19
.= (dom (the_arity_of o)) /\ (dom x) by A12, RELAT_1:27 ;
hence (proj (A,i)) # x = (commute x) . i by A11, A5, SS; :: thesis: verum