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

now :: thesis:

let s9 be object ; :: thesis:
assume A3: s9 in the carrier of S ; :: thesis:
then reconsider s99 = s9 as SortSymbol of S ;
(commute F) . s9 in Funcs (I,(Funcs (( the Sorts of U1 . s9),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A1, A3, Th26;
then commute ((commute F) . s9) in Funcs (( the Sorts of U1 . s9),(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A3, FUNCT_6:55;
then H . s9 in Funcs (( the Sorts of U1 . s9),(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A2, A3;
then consider Hs being Function such that
A4: Hs = H . s9 and
A5: dom Hs = the Sorts of U1 . s9 and
A6: rng Hs c= Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) by FUNCT_2:def 2;
rng Hs c= the Sorts of (product A) . s9

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: x in rng Hs ; :: thesis:
then consider f being Function such that
A8: f = x and
A9: dom f = I and
rng f c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } by A6, FUNCT_2:def 2;
consider x1 being object such that
A10: x1 in dom Hs and
A11: Hs . x1 = f by A7, A8, FUNCT_1:def 3;

A12: now :: thesis:

let i9 be object ; :: thesis:
assume i9 in dom (Carrier (A,s99)) ; :: thesis:
then reconsider i99 = i9 as Element of I ;
consider F9 being ManySortedFunction of U1,(A . i99) such that
A13: F9 = F . i99 and
F9 is_homomorphism U1,A . i99 by A1;
H . s99 = commute ((commute F) . s99) by A2;
then A14: f . i99 = (F9 . s99) . x1 by A1, A4, A5, A10, A11, A13, Th27;
dom (F9 . s99) = dom Hs by A5, FUNCT_2:def 1;
then A15: (F9 . s9) . x1 in rng (F9 . s9) by A10, FUNCT_1:def 3;
( ex U0 being MSAlgebra over S st
( U0 = A . i99 & (Carrier (A,s99)) . i99 = the Sorts of U0 . s99 ) & rng (F9 . s99) c= the Sorts of (A . i99) . s99 ) by PRALG_2:def 9;
hence f . i9 in (Carrier (A,s99)) . i9 by A14, A15; :: thesis:

end;

dom (Carrier (A,s99)) = dom f by A9, PARTFUN1:def 2;
then f in product (Carrier (A,s99)) by A12, CARD_3:9;
hence x in the Sorts of (product A) . s9 by A8, PRALG_2:def 10; :: thesis:

end;

hence H . s9 is Function of ( the Sorts of U1 . s9),( the Sorts of (product A) . s9) by A3, A4, A5, FUNCT_2:def 1, RELSET_1:4; :: thesis:

end;

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

proof

let o be OperSymbol of S; :: according to MSUALG_3:def 7 :: thesis:
assume Args (o,U1) <> {} ; :: thesis:
let x be Element of Args (o,U1); :: thesis:
set s9 = the_result_sort_of o;
A17: Result (o,U1) = the Sorts of U1 . (the_result_sort_of o) by PRALG_2:3;
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:4;
then A20: x = {} by TARSKI:def 1;

A21: now :: thesis:

let i9 be object ; :: thesis:
assume i9 in I ; :: thesis:
then reconsider ii = i9 as Element of I ;
consider F1 being ManySortedFunction of U1,(A . ii) such that
A22: F1 = F . ii and
A23: F1 is_homomorphism U1,A . ii by A1;
A24: F1 # x = {} by A19, A20, Th11;
thus ((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) . i9 = (F1 . (the_result_sort_of o)) . ((Den (o,U1)) . x) by A1, A17, A20, A22, Th27
.= const (o,(A . ii)) by A23, A24
.= (const (o,(product A))) . i9 by A19, Th9 ; :: thesis:

end;

const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i1))) where i1 is Element of I : verum } )) by A19, Th8;
then A25: ex Co being Function st
( 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;
(commute ((commute F) . (the_result_sort_of o))) . (const (o,U1)) in product (Carrier (A,(the_result_sort_of o))) by A1, A18, A20, Th28;
then dom ((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) = I by PARTFUN1:def 2;
then A26: (commute ((commute F) . (the_result_sort_of o))) . (const (o,U1)) = const (o,(product A)) by A25, A21;
H # x = {} by A19, A20, Th11;
hence (H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x) by A2, A20, A26; :: thesis:

end;

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

A28: Den (o,(product A)) = (OPS A) . o by MSUALG_1:def 6
.= IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by PRALG_2:def 13
.= Commute (Frege (A ?. o)) by A27, FUNCOP_1:def 8 ;

A29: now :: thesis:

let y be Element of Args (o,(product A)); :: thesis:
commute y in product (doms (A ?. o)) by A27, Th17;
then A30: commute y in dom (Frege (A ?. o)) by PARTFUN1:def 2;
y in dom (Commute (Frege (A ?. o))) by A27, Th18;
then (Den (o,(product A))) . y = (Frege (A ?. o)) . (commute y) by A28, PRALG_2:def 1;
hence (Den (o,(product A))) . y in rng (Frege (A ?. o)) by A30, FUNCT_1:def 3; :: thesis:

end;

then reconsider f1 = (Den (o,(product A))) . (H # x) as Function by PRALG_2:8;
f1 in rng (Frege (A ?. o)) by A29;
then A31: dom f1 = I by PRALG_2:9;
set D = union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } ;
set f = (commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x);
A32: H # x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } )))) by Th14;

A33: now :: thesis:

let i9 be object ; :: thesis:
assume i9 in I ; :: thesis:
then reconsider ii = i9 as Element of I ;
consider F1 being ManySortedFunction of U1,(A . ii) such that
A34: F1 = F . ii and
A35: F1 is_homomorphism U1,A . ii by A1;
A36: (F1 . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(A . ii))) . (F1 # x) by A35;
x in Args (o,U1) ;
then A40: x in product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;
then A41: dom x = dom ( the Sorts of U1 * (the_arity_of o)) by CARD_3:9;
A42: dom x = dom (the_arity_of o) by MSUALG_6:2;

A37: now :: thesis:

let n be object ; :: thesis:
assume A38: n in dom (the_arity_of o) ; :: thesis:
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 Element of the carrier of S ;
A39: (F1 # x) . n = (F1 . ((the_arity_of o) /. n)) . (x . n) by A38, Th13
.= (F1 . s1) . (x . n) by A38, PARTFUN1:def 6 ;
x . n in ( the Sorts of U1 * (the_arity_of o)) . n by A38, A40, A41, A42, CARD_3:9;
then A43: x . n in the Sorts of U1 . s1 by A38, A42, A41, FUNCT_1:12;
A44: (H # x) . n = (H . ((the_arity_of o) /. n)) . (x . n) by A38, Th13
.= (H . s1) . (x . n) by A38, PARTFUN1:def 6
.= (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 A32, A38, FUNCT_6:56
.= (F1 # x) . n by A1, A34, A43, A39, A44, Th27 ; :: thesis:

end;

dom F1 = the carrier of S by PARTFUN1:def 2;
then A45: rng (the_arity_of o) c= dom F1 ;
commute (H # x) in Funcs (I,(Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } )))) by A27, A32, FUNCT_6:55;
then consider ff being Function such that
A46: ff = commute (H # x) and
A47: dom ff = I and
A48: rng ff c= Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } )) by FUNCT_2:def 2;
ff . ii in rng ff by A47, FUNCT_1:def 3;
then A49: ex gg being Function st
( gg = (commute (H # x)) . ii & dom gg = dom (the_arity_of o) & rng gg c= union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } ) by A46, A48, FUNCT_2:def 2;
A50: x in product (doms (F1 * (the_arity_of o))) by Th12;
dom (F1 # x) = dom ((Frege (F1 * (the_arity_of o))) . x) by MSUALG_3:def 5
.= dom ((F1 * (the_arity_of o)) .. x) by A50, PRALG_2:def 2
.= (dom (F1 * (the_arity_of o))) /\ (dom x) by PRALG_1:def 19
.= (dom (the_arity_of o)) /\ (dom x) by A45, RELAT_1:27
.= dom (the_arity_of o) by A42 ;
then F1 # x = (commute (H # x)) . ii by A49, A37;
then ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 = (Den (o,(A . ii))) . ((commute (H # x)) . ii) by A1, A17, A34, A36, Th27
.= f1 . i9 by A27, Th22 ;
hence ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 = f1 . i9 ; :: thesis:

end;

(commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x) in product (Carrier (A,(the_result_sort_of o))) by A1, A17, Th28;
then dom ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) = I by PARTFUN1:def 2;
then (commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x) = f1 by A31, A33;
hence (H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x) by A2; :: thesis:

end;

take H ; :: thesis:
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
A51: F1 = F . i and
F1 is_homomorphism U1,A . i by A1;
A52: dom ((proj (A,i)) ** H) = (dom (proj (A,i))) /\ (dom H) by PBOOLE:def 19
.= the carrier of S /\ (dom H) by PARTFUN1:def 2
.= the carrier of S /\ the carrier of S by PARTFUN1:def 2
.= the carrier of S ;

A53: now :: thesis:

let s9 be object ; :: thesis:
assume s9 in the carrier of S ; :: thesis:
then reconsider s1 = s9 as SortSymbol of S ;
A54: ((proj (A,i)) ** H) . s9 = ((proj (A,i)) . s1) * (H . s1) by A52, PBOOLE:def 19
.= (proj ((Carrier (A,s1)),i)) * (H . s1) by Def2
.= (proj ((Carrier (A,s1)),i)) * (commute ((commute F) . s1)) by A2 ;
(commute F) . s1 in Funcs (I,(Funcs (( the Sorts of U1 . s1),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A1, Th26;
then commute ((commute F) . s1) in Funcs (( the Sorts of U1 . s1),(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by FUNCT_6:55;
then consider f9 being Function such that
A55: f9 = commute ((commute F) . s1) and
A56: dom f9 = the Sorts of U1 . s1 and
rng f9 c= Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) by FUNCT_2:def 2;
rng f9 c= dom (proj ((Carrier (A,s1)),i))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f9 ; :: thesis:
then consider x9 being object such that
A57: x9 in dom f9 and
A58: f9 . x9 = y by FUNCT_1:def 3;
(commute ((commute F) . s1)) . x9 in product (Carrier (A,s1)) by A1, A56, A57, Th28;
hence y in dom (proj ((Carrier (A,s1)),i)) by A55, A58, CARD_3:def 16; :: thesis:

end;

then A59: dom (((proj (A,i)) ** H) . s9) = the Sorts of U1 . s9 by A55, A56, A54, RELAT_1:27;

A60: now :: thesis:

let x be object ; :: thesis:
assume A61: x in the Sorts of U1 . s9 ; :: thesis:
then (commute ((commute F) . s1)) . x in product (Carrier (A,s1)) by A1, Th28;
then A62: (commute ((commute F) . s1)) . x in dom (proj ((Carrier (A,s1)),i)) by CARD_3:def 16;
thus (((proj (A,i)) ** H) . s9) . x = (proj ((Carrier (A,s1)),i)) . ((commute ((commute F) . s1)) . x) by A54, A59, A61, FUNCT_1:12
.= ((commute ((commute F) . s1)) . x) . i by A62, CARD_3:def 16
.= (F1 . s9) . x by A1, A51, A61, Th27 ; :: thesis:

end;

dom (F1 . s9) = dom (F1 . s1)
.= the Sorts of U1 . s9 by FUNCT_2:def 1 ;
hence ((proj (A,i)) ** H) . s9 = F1 . s9 by A59, A60; :: thesis:

end;

dom F1 = the carrier of S by PARTFUN1:def 2;
hence (proj (A,i)) ** H = F . i by A51, A52, A53; :: 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: