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 Args o,(product A) <> {} & 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 Args o,(product A) <> {} & 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 Args o,(product A) <> {} & 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 Args o,(product A) <> {} & 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: ( Args o,(product A) <> {} & the_arity_of o <> {} implies for i being Element of I holds (proj A,i) # x = (commute x) . i )
assume A1: ( Args o,(product A) <> {} & the_arity_of o <> {} ) ; :: thesis: for i being Element of I holds (proj A,i) # x = (commute x) . i
let i be Element of I; :: thesis: (proj A,i) # x = (commute x) . i
set C = union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ;
dom (proj A,i) = the carrier of S by PARTFUN1:def 4;
then A2: rng (the_arity_of o) c= dom (proj A,i) ;
A3: dom (the_arity_of o) <> {} by A1;
A4: x in Funcs (dom (the_arity_of o)),(Funcs I,(union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } )) by Th15;
then commute x in Funcs I,(Funcs (dom (the_arity_of o)),(union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } )) by A3, FUNCT_6:85;
then A5: ( dom (commute x) = I & rng (commute x) c= Funcs (dom (the_arity_of o)),(union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ) ) by FUNCT_2:169;
then (commute x) . i in rng (commute x) by FUNCT_1:def 5;
then A6: dom ((commute x) . i) = dom (the_arity_of o) by A5, FUNCT_2:169;
A7: x in product (doms ((proj A,i) * (the_arity_of o))) by Th13;
A8: 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 A7, PRALG_2:def 8
.= dom ((proj A,i) * (the_arity_of o)) by PRALG_1:def 17
.= dom (the_arity_of o) by A2, RELAT_1:46 ;

now

let n be set ; :: thesis: ( n in dom (the_arity_of o) implies ((proj A,i) # x) . n = ((commute x) . i) . n )
assume A9: n in dom (the_arity_of o) ; :: thesis: ((proj A,i) # x) . n = ((commute x) . i) . n
A10: ( dom x = dom (the_arity_of o) & rng x c= Funcs I,(union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ) ) by A4, FUNCT_2:169;
n in dom x by A4, A9, FUNCT_2:169;
then x . n in rng x by FUNCT_1:def 5;
then consider g being Function such that
A11: ( g = x . n & dom g = I & rng g c= union { (the Sorts of (A . i') . s') where i' is Element of I, s' is Element of the carrier of S : verum } ) by A10, FUNCT_2:def 2;
x . n in product (Carrier A,((the_arity_of o) /. n)) by A9, Th16;
then A12: x . n in dom (proj (Carrier A,((the_arity_of o) /. n)),i) by Def2;
thus ((proj A,i) # x) . n = ((proj A,i) . ((the_arity_of o) /. n)) . (x . n) by A9, Th14
.= (proj (Carrier A,((the_arity_of o) /. n)),i) . (x . n) by Def3
.= g . i by A11, A12, Def2
.= ((commute x) . i) . n by A4, A9, A11, FUNCT_6:86 ; :: thesis: verum

end;

hence (proj A,i) # x = (commute x) . i by A6, A8, FUNCT_1:9; :: thesis: verum