let I be non empty set ; :: thesis:
let S be non empty non void ManySortedSign ; :: thesis:
let A be MSAlgebra-Family of I,S; :: thesis:
let U1 be non-empty MSAlgebra of S; :: thesis:
let F be ManySortedFunction of ; :: thesis:
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:
deffunc H₁( Element of S) -> set = commute ((commute F) . $1);
consider H being ManySortedSet of such that
A2: for s' being Element of the carrier of S holds H . s' = H₁(s') from PBOOLE:sch 5();
set SU = the Sorts of U1;
set CA = the carrier of S;
set SA = union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of S : verum } ;

now

let s' be set ; :: thesis:
assume A3: s' in the carrier of S ; :: thesis:
then s' in dom the Sorts of U1 by PARTFUN1:def 4;
then A4: the Sorts of U1 . s' <> {} ;
reconsider s'' = s' as SortSymbol of S by A3;
(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, A3, 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 A4, FUNCT_6:85;
then H . 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 A2, A3;
then consider Hs being Function such that
A5: ( Hs = H . s' & dom Hs = the Sorts of U1 . s' & rng Hs 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;
s' in dom (SORTS A) by A3, PARTFUN1:def 4;
then A6: not (SORTS A) . s' is empty ;
rng Hs c= the Sorts of (product A) . s'

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A7: x in rng Hs ; :: thesis:
then consider f being Function such that
A8: ( f = 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 A5, FUNCT_2:def 2;
A9: dom (Carrier A,s'') = dom f by A8, PARTFUN1:def 4;
consider x1 being set such that
A10: ( x1 in dom Hs & Hs . x1 = f ) by A7, A8, FUNCT_1:def 5;

now

let i' be set ; :: thesis:
assume i' in dom (Carrier A,s'') ; :: thesis:
then reconsider i'' = i' as Element of I by PARTFUN1:def 4;
A11: H . s'' = commute ((commute F) . s'') by A2;
consider F' being ManySortedFunction of U1,(A . i'') such that
A12: ( F' = F . i'' & F' is_homomorphism U1,A . i'' ) by A1;
A13: f . i'' = (F' . s'') . x1 by A1, A5, A10, A11, A12, Th28;
consider U0 being MSAlgebra of S such that
A14: ( U0 = A . i'' & (Carrier A,s'') . i'' = the Sorts of U0 . s'' ) by PRALG_2:def 16;
A15: rng (F' . s'') c= the Sorts of (A . i'') . s'' ;
dom (F' . s'') = dom Hs by A5, FUNCT_2:def 1;
then (F' . s') . x1 in rng (F' . s') by A10, FUNCT_1:def 5;
hence f . i' in (Carrier A,s'') . i' by A13, A14, A15; :: thesis:

end;

then f in product (Carrier A,s'') by A9, CARD_3:18;
hence x in the Sorts of (product A) . s' by A8, PRALG_2:def 17; :: thesis:

end;

hence H . s' is Function of (the Sorts of U1 . s'),(the Sorts of (product A) . s') by A5, A6, FUNCT_2:def 1, RELSET_1:11; :: thesis:

end;

then reconsider H = H as ManySortedFunction of U1,(product A) by PBOOLE:def 18;
take H ; :: thesis:
A16: H is_homomorphism U1, product A

proof

let o be OperSymbol of S; :: according to MSUALG_3:def 9 :: thesis:
assume Args o,U1 <> {} ; :: thesis:
let x be Element of Args o,U1; :: thesis:
set s' = the_result_sort_of o;
A17: Result o,U1 = the Sorts of U1 . (the_result_sort_of o) by PRALG_2:10;
then A18: (Den o,U1) . x in the Sorts of U1 . (the_result_sort_of o) ;
thus (H . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(product A)) . (H # x) :: thesis:

proof

per cases ;

suppose A19: the_arity_of o = {} ; :: thesis:

set f = (commute ((commute F) . (the_result_sort_of o))) . (const o,U1);
Args o,U1 = {{} } by A19, PRALG_2:11;
then A20: x = {} by TARSKI:def 1;
then A21: H # x = {} by A19, Th12;
(commute ((commute F) . (the_result_sort_of o))) . (const o,U1) in product (Carrier A,(the_result_sort_of o)) by A1, A18, A20, Th29;
then A22: dom ((commute ((commute F) . (the_result_sort_of o))) . (const o,U1)) = dom (Carrier A,(the_result_sort_of o)) by CARD_3:18
.= I by PARTFUN1:def 4 ;
const o,(product A) in Funcs I,(union { (Result o,(A . i1)) where i1 is Element of I : verum } ) by A19, Th9;
then consider Co being Function such that
A23: ( Co = const o,(product A) & dom Co = I & rng Co c= union { (Result o,(A . i1)) where i1 is Element of I : verum } ) by FUNCT_2:def 2;

now

let i' be set ; :: thesis:
assume i' in I ; :: thesis:
then reconsider ii = i' as Element of I ;
consider F1 being ManySortedFunction of U1,(A . ii) such that
A24: ( F1 = F . ii & F1 is_homomorphism U1,A . ii ) by A1;
A25: F1 # x = {} by A19, A20, Th12;
thus ((commute ((commute F) . (the_result_sort_of o))) . (const o,U1)) . i' = (F1 . (the_result_sort_of o)) . ((Den o,U1) . x) by A1, A17, A20, A24, Th28
.= const o,(A . ii) by A24, A25, MSUALG_3:def 9
.= (const o,(product A)) . i' by A19, Th10 ; :: thesis:

end;

then (commute ((commute F) . (the_result_sort_of o))) . (const o,U1) = const o,(product A) by A22, A23, FUNCT_1:9;
hence (H . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(product A)) . (H # x) by A2, A20, A21; :: thesis:

end;

suppose A26: the_arity_of o <> {} ; :: thesis:

set f = (commute ((commute F) . (the_result_sort_of o))) . ((Den o,U1) . x);
A27: Den o,(product A) = (OPS A) . o by MSUALG_1:def 11
.= IFEQ (the_arity_of o),{} ,(commute (A ?. o)),(Commute (Frege (A ?. o))) by PRALG_2:def 20
.= Commute (Frege (A ?. o)) by A26, FUNCOP_1:def 8 ;

A28: now

let y be Element of Args o,(product A); :: thesis:
y in dom (Commute (Frege (A ?. o))) by A26, Th19;
then A29: (Den o,(product A)) . y = (Frege (A ?. o)) . (commute y) by A27, PRALG_2:def 6;
commute y in product (doms (A ?. o)) by A26, Th18;
then commute y in dom (Frege (A ?. o)) by PARTFUN1:def 4;
hence (Den o,(product A)) . y in rng (Frege (A ?. o)) by A29, FUNCT_1:def 5; :: thesis:

end;

then reconsider f1 = (Den o,(product A)) . (H # x) as Function by PRALG_2:15;
set D = union { (the Sorts of (A . i') . ss) where i' is Element of I, ss is Element of the carrier of S : verum } ;
A30: H # x in Funcs (dom (the_arity_of o)),(Funcs I,(union { (the Sorts of (A . i') . ss) where i' is Element of I, ss is Element of the carrier of S : verum } )) by Th15;
(commute ((commute F) . (the_result_sort_of o))) . ((Den o,U1) . x) in product (Carrier A,(the_result_sort_of o)) by A1, A17, Th29;
then A31: dom ((commute ((commute F) . (the_result_sort_of o))) . ((Den o,U1) . x)) = dom (Carrier A,(the_result_sort_of o)) by CARD_3:18
.= I by PARTFUN1:def 4 ;
f1 in rng (Frege (A ?. o)) by A28;
then A32: dom f1 = I by PRALG_2:16;

now

let i' be set ; :: thesis:
assume i' in I ; :: thesis:
then reconsider ii = i' as Element of I ;
consider F1 being ManySortedFunction of U1,(A . ii) such that
A33: ( F1 = F . ii & F1 is_homomorphism U1,A . ii ) by A1;
A34: (F1 . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(A . ii)) . (F1 # x) by A33, MSUALG_3:def 9;
dom F1 = the carrier of S by PARTFUN1:def 4;
then A35: rng (the_arity_of o) c= dom F1 ;
A36: x in product (doms (F1 * (the_arity_of o))) by Th13;
A37: dom (F1 # x) = dom ((Frege (F1 * (the_arity_of o))) . x) by MSUALG_3:def 7
.= dom ((F1 * (the_arity_of o)) .. x) by A36, PRALG_2:def 8
.= dom (F1 * (the_arity_of o)) by PRALG_1:def 17
.= dom (the_arity_of o) by A35, RELAT_1:46 ;
dom (the_arity_of o) <> {} by A26;
then commute (H # x) in Funcs I,(Funcs (dom (the_arity_of o)),(union { (the Sorts of (A . i') . ss) where i' is Element of I, ss is Element of the carrier of S : verum } )) by A30, FUNCT_6:85;
then consider ff being Function such that
A38: ( ff = commute (H # x) & dom ff = I & rng ff c= Funcs (dom (the_arity_of o)),(union { (the Sorts of (A . i') . ss) where i' is Element of I, ss is Element of the carrier of S : verum } ) ) by FUNCT_2:def 2;
ff . ii in rng ff by A38, FUNCT_1:def 5;
then consider gg being Function such that
A39: ( gg = (commute (H # x)) . ii & dom gg = dom (the_arity_of o) & rng gg c= union { (the Sorts of (A . i') . ss) where i' is Element of I, ss is Element of the carrier of S : verum } ) by A38, FUNCT_2:def 2;

now

let n be set ; :: thesis:
assume A40: n in dom (the_arity_of o) ; :: thesis:
then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def 5;
then reconsider s1 = (the_arity_of o) . n as Element of the carrier of S ;
x in Args o,U1 ;
then A41: x in product (the Sorts of U1 * (the_arity_of o)) by PRALG_2:10;
then A42: dom x = dom (the Sorts of U1 * (the_arity_of o)) by CARD_3:18
.= dom (the_arity_of o) by PRALG_2:10 ;
A43: dom x = dom (the Sorts of U1 * (the_arity_of o)) by A41, CARD_3:18;
then x . n in (the Sorts of U1 * (the_arity_of o)) . n by A40, A41, A42, CARD_3:18;
then A44: x . n in the Sorts of U1 . s1 by A40, A42, A43, FUNCT_1:22;
A45: (F1 # x) . n = (F1 . ((the_arity_of o) /. n)) . (x . n) by A40, Th14
.= (F1 . s1) . (x . n) by A40, PARTFUN1:def 8 ;
A46: (H # x) . n = (H . ((the_arity_of o) /. n)) . (x . n) by A40, Th14
.= (H . s1) . (x . n) by A40, PARTFUN1:def 8
.= (commute ((commute F) . s1)) . (x . n) by A2 ;
then reconsider g = (H # x) . n as Function ;
thus ((commute (H # x)) . ii) . n = g . ii by A30, A40, FUNCT_6:86
.= (F1 # x) . n by A1, A33, A44, A45, A46, Th28 ; :: thesis:

end;

then F1 # x = (commute (H # x)) . ii by A37, A39, FUNCT_1:9;
then ((commute ((commute F) . (the_result_sort_of o))) . ((Den o,U1) . x)) . i' = (Den o,(A . ii)) . ((commute (H # x)) . ii) by A1, A17, A33, A34, Th28
.= f1 . i' by A26, Th23 ;
hence ((commute ((commute F) . (the_result_sort_of o))) . ((Den o,U1) . x)) . i' = f1 . i' ; :: thesis:

end;

then (commute ((commute F) . (the_result_sort_of o))) . ((Den o,U1) . x) = f1 by A31, A32, FUNCT_1:9;
hence (H . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(product A)) . (H # x) by A2; :: thesis:

end;

for i being Element of I holds (proj A,i) ** H = F . i

proof

let i be Element of I; :: thesis:
consider F1 being ManySortedFunction of U1,(A . i) such that
A47: ( F1 = F . i & F1 is_homomorphism U1,A . i ) by A1;
A48: dom ((proj A,i) ** H) = (dom (proj A,i)) /\ (dom H) by PBOOLE:def 24
.= the carrier of S /\ (dom H) by PARTFUN1:def 4
.= the carrier of S /\ the carrier of S by PARTFUN1:def 4
.= the carrier of S ;
A49: dom F1 = the carrier of S by PARTFUN1:def 4;

now

let s' be set ; :: thesis:
assume s' in the carrier of S ; :: thesis:
then reconsider s1 = s' as SortSymbol of S ;
(commute F) . s1 in Funcs I,(Funcs (the Sorts of U1 . s1),(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) . s1) in Funcs (the Sorts of U1 . s1),(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
A50: ( f' = commute ((commute F) . s1) & dom f' = the Sorts of U1 . s1 & 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;
A51: rng f' c= dom (proj (Carrier A,s1),i)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f' ; :: thesis:
then consider x' being set such that
A52: ( x' in dom f' & f' . x' = y ) by FUNCT_1:def 5;
(commute ((commute F) . s1)) . x' in product (Carrier A,s1) by A1, A50, A52, Th29;
hence y in dom (proj (Carrier A,s1),i) by A50, A52, Def2; :: thesis:

end;

A53: ((proj A,i) ** H) . s' = ((proj A,i) . s1) * (H . s1) by A48, PBOOLE:def 24
.= (proj (Carrier A,s1),i) * (H . s1) by Def3
.= (proj (Carrier A,s1),i) * (commute ((commute F) . s1)) by A2 ;
then A54: dom (((proj A,i) ** H) . s') = the Sorts of U1 . s' by A50, A51, RELAT_1:46;
A55: dom (F1 . s') = dom (F1 . s1)
.= the Sorts of U1 . s' by FUNCT_2:def 1 ;

now

let x be set ; :: thesis:
assume A56: x in the Sorts of U1 . s' ; :: thesis:
then (commute ((commute F) . s1)) . x in product (Carrier A,s1) by A1, Th29;
then A57: (commute ((commute F) . s1)) . x in dom (proj (Carrier A,s1),i) by Def2;
thus (((proj A,i) ** H) . s') . x = (proj (Carrier A,s1),i) . ((commute ((commute F) . s1)) . x) by A53, A54, A56, FUNCT_1:22
.= ((commute ((commute F) . s1)) . x) . i by A57, Def2
.= (F1 . s') . x by A1, A47, A56, Th28 ; :: thesis:

end;

hence ((proj A,i) ** H) . s' = F1 . s' by A54, A55, FUNCT_1:9; :: thesis:

end;

hence (proj A,i) ** H = F . i by A47, A48, A49, FUNCT_1:9; :: thesis:

end;

hence ( H is_homomorphism U1, product A & ( for i being Element of I holds (proj A,i) ** H = F . i ) ) by A16; :: thesis: