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 y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
let A be MSAlgebra-Family of I,S; :: thesis: for o being OperSymbol of S
for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
let o be OperSymbol of S; :: thesis: for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
let y be Element of Args (o,(product A)); :: thesis: ( the_arity_of o <> {} implies commute y in product (doms (A ?. o)) )
set D = union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ;
A1: y 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;
assume the_arity_of o <> {} ; :: thesis: commute y in product (doms (A ?. o))
then commute y 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 A2: ex f being Function st
( f = commute y & dom f = I & rng f 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 FUNCT_2:def 2;

A3: now :: thesis: for i1 being object st i1 in dom (doms (A ?. o)) holds
(commute y) . i1 in (doms (A ?. o)) . i1

let i1 be object ; :: thesis: ( i1 in dom (doms (A ?. o)) implies (commute y) . i1 in (doms (A ?. o)) . i1 )
assume i1 in dom (doms (A ?. o)) ; :: thesis: (commute y) . i1 in (doms (A ?. o)) . i1
then reconsider ii = i1 as Element of I by PRALG_2:11;

A4: now :: thesis: for n being object st n in dom ( the Sorts of (A . ii) * (the_arity_of o)) holds
((commute y) . ii) . n in ( the Sorts of (A . ii) * (the_arity_of o)) . n

let n be object ; :: thesis: ( n in dom ( the Sorts of (A . ii) * (the_arity_of o)) implies ((commute y) . ii) . n in ( the Sorts of (A . ii) * (the_arity_of o)) . n )
assume A5: n in dom ( the Sorts of (A . ii) * (the_arity_of o)) ; :: thesis: ((commute y) . ii) . n in ( the Sorts of (A . ii) * (the_arity_of o)) . n
then A6: n in dom (the_arity_of o) by PRALG_2:3;
then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def 3;
then reconsider s1 = (the_arity_of o) . n as SortSymbol of S ;
A7: ex ff being Function st
( ff = y & dom ff = dom (the_arity_of o) & rng ff 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 A1, FUNCT_2:def 2;
then n in dom y by A5, PRALG_2:3;
then y . n in rng y by FUNCT_1:def 3;
then consider g being Function such that
A8: g = y . 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 A7, FUNCT_2:def 2;
( ((commute y) . ii) . n = g . ii & g . ii in the Sorts of (A . ii) . s1 ) by A1, A6, A8, Th16, FUNCT_6:56;
hence ((commute y) . ii) . n in ( the Sorts of (A . ii) * (the_arity_of o)) . n by A5, FUNCT_1:12; :: thesis: verum

end;

(commute y) . ii in rng (commute y) by A2, FUNCT_1:def 3;
then ex h being Function st
( h = (commute y) . ii & dom h = dom (the_arity_of o) & rng h c= 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:def 2;
then dom ((commute y) . ii) = dom ( the Sorts of (A . ii) * (the_arity_of o)) by PRALG_2:3;
then (commute y) . ii in product ( the Sorts of (A . ii) * (the_arity_of o)) by A4, CARD_3:9;
then (commute y) . ii in Args (o,(A . ii)) by PRALG_2:3;
hence (commute y) . i1 in (doms (A ?. o)) . i1 by PRALG_2:11; :: thesis: verum

end;

dom (commute y) = dom (doms (A ?. o)) by A2, PRALG_2:11;
hence commute y in product (doms (A ?. o)) by A3, CARD_3:9; :: thesis: verum