let I be non empty set ; :: thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s)
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s)
let A be MSAlgebra-Family of I,S; :: thesis: for s being SortSymbol of S
for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s)
let s be SortSymbol of S; :: thesis: for U1 being non-empty MSAlgebra of S
for F being ManySortedFunction of st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s)
let U1 be non-empty MSAlgebra of S; :: thesis: for F being ManySortedFunction of st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s)
let F be ManySortedFunction of ; :: thesis: ( ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s) )
assume A1: for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ; :: thesis: for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier A,s)
let x be set ; :: thesis: ( x in the Sorts of U1 . s implies (commute ((commute F) . s)) . x in product (Carrier A,s) )
assume A2: x in the Sorts of U1 . s ; :: thesis: (commute ((commute F) . s)) . x in product (Carrier A,s)
set SU = the Sorts of U1;
set SA = union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum } ;
(commute F) . s in Funcs I,(Funcs (the Sorts of U1 . s),(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum } )) by A1, Th27;
then commute ((commute F) . s) in Funcs (the Sorts of U1 . s),(Funcs I,(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum } )) by FUNCT_6:85;
then consider f' being Function such that
A3: ( f' = commute ((commute F) . s) & dom f' = the Sorts of U1 . s & rng f' c= Funcs I,(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum } ) ) by FUNCT_2:def 2;
f' . x in rng f' by A2, A3, FUNCT_1:def 5;
then consider f being Function such that
A4: ( f = (commute ((commute F) . s)) . x & dom f = I & rng f c= union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum } ) by A3, FUNCT_2:def 2;
A5: dom ((commute ((commute F) . s)) . x) = dom (Carrier A,s) by A4, PARTFUN1:def 4;

now

let i1 be set ; :: thesis: ( i1 in dom (Carrier A,s) implies ((commute ((commute F) . s)) . x) . i1 in (Carrier A,s) . i1 )
assume i1 in dom (Carrier A,s) ; :: thesis: ((commute ((commute F) . s)) . x) . i1 in (Carrier A,s) . i1
then reconsider i' = i1 as Element of I by PARTFUN1:def 4;
consider F1 being ManySortedFunction of U1,(A . i') such that
A6: ( F1 = F . i' & F1 is_homomorphism U1,A . i' ) by A1;
A7: f . i' = (F1 . s) . x by A1, A2, A4, A6, Th28;
consider U0 being MSAlgebra of S such that
A8: ( U0 = A . i' & (Carrier A,s) . i' = the Sorts of U0 . s ) by PRALG_2:def 16;
x in dom (F1 . s) by A2, FUNCT_2:def 1;
then (F1 . s) . x in rng (F1 . s) by FUNCT_1:def 5;
hence ((commute ((commute F) . s)) . x) . i1 in (Carrier A,s) . i1 by A4, A7, A8; :: thesis: verum

end;

hence (commute ((commute F) . s)) . x in product (Carrier A,s) by A5, CARD_3:18; :: thesis: verum