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 EqR be Equivalence_Relation of I; :: thesis:
set U1 = product A;
set U2 = product (product (A / EqR));
set U19 = the Sorts of (product A);
set U29 = the Sorts of (product (product (A / EqR)));
defpred S₁[ object , object , object ] means for f1, g1 being Function st f1 = $2 & g1 = $1 holds
for e being Element of Class EqR holds g1 . e = f1 | e;
A1: for s being object st s in the carrier of S holds
for x being object st x in the Sorts of (product A) . s holds
ex y being object st
( y in the Sorts of (product (product (A / EqR))) . s & S₁[y,x,s] )

proof

let s be object ; :: thesis:
assume s in the carrier of S ; :: thesis:
then reconsider s9 = s as SortSymbol of S ;
A2: the Sorts of (product A) . s9 = product (Carrier (A,s9)) by PRALG_2:def 10;
let x be object ; :: thesis:
assume A3: x in the Sorts of (product A) . s ; :: thesis:
reconsider x = x as Function by A3, A2;
deffunc H₁( set ) -> set = x | $1;
consider y being ManySortedSet of Class EqR such that
A4: for c being set st c in Class EqR holds
y . c = H₁(c) from PBOOLE:sch 7();
A5: dom (Carrier ((product (A / EqR)),s9)) = Class EqR by PARTFUN1:def 2;
A6: for a being object st a in dom (Carrier ((product (A / EqR)),s9)) holds
y . a in (Carrier ((product (A / EqR)),s9)) . a

proof

set A9 = product (A / EqR);
let a be object ; :: thesis:
assume A7: a in dom (Carrier ((product (A / EqR)),s9)) ; :: thesis:
reconsider a = a as set by TARSKI:1;
A8: (A / EqR) . a = A | a by A7, Def4;
reconsider a = a as non empty Subset of I by A5, A7;
A9: ex U0 being MSAlgebra over S st
( U0 = (product (A / EqR)) . a & (Carrier ((product (A / EqR)),s9)) . a = the Sorts of U0 . s9 ) by A7, PRALG_2:def 9;
A10: dom (A | a) = (dom A) /\ a by RELAT_1:61
.= I /\ a by PARTFUN1:def 2
.= a by XBOOLE_1:28 ;
then reconsider Aa1 = A | a as ManySortedSet of a by PARTFUN1:def 2;
for i being object st i in a holds
Aa1 . i is non-empty MSAlgebra over S

proof

let i be object ; :: thesis:
assume A11: i in a ; :: thesis:
then A . i is non-empty MSAlgebra over S by PRALG_2:def 5;
hence Aa1 . i is non-empty MSAlgebra over S by A10, A11, FUNCT_1:47; :: thesis:

end;

then reconsider Aa = Aa1 as MSAlgebra-Family of a,S by PRALG_2:def 5;
x | a in product ((Carrier (A,s9)) | a) by A3, A2, Th1;
then A12: x | a in product (Carrier (Aa,s9)) by Th2;
consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that
A13: Ji = (id (Class EqR)) . a and
A14: ( Cs = (A / EqR) . a & (product (A / EqR)) . a = product Cs ) by A7, Def5;
Ji = a by A7, A13, FUNCT_1:18;
then (Carrier ((product (A / EqR)),s9)) . a = product (Carrier (Aa,s9)) by A8, A14, A9, PRALG_2:def 10;
hence y . a in (Carrier ((product (A / EqR)),s9)) . a by A4, A7, A12; :: thesis:

end;

take y ; :: thesis:
dom (Carrier ((product (A / EqR)),s9)) = Class EqR by PARTFUN1:def 2
.= dom y by PARTFUN1:def 2 ;
then y in product (Carrier ((product (A / EqR)),s9)) by A6, CARD_3:9;
hence ( y in the Sorts of (product (product (A / EqR))) . s & S₁[y,x,s] ) by A4, PRALG_2:def 10; :: thesis:

end;

consider F being ManySortedFunction of the Sorts of (product A), the Sorts of (product (product (A / EqR))) such that
A15: for s being object st s in the carrier of S holds
ex f being Function of ( the Sorts of (product A) . s),( the Sorts of (product (product (A / EqR))) . s) st
( f = F . s & ( for x being object st x in the Sorts of (product A) . s holds
S₁[f . x,x,s] ) ) from MSSUBFAM:sch 1(A1);
A16: F is_homomorphism product A, product (product (A / EqR))

proof

let o be OperSymbol of S; :: according to MSUALG_3:def 7 :: thesis:
assume Args (o,(product A)) <> {} ; :: thesis:
let x be Element of Args (o,(product A)); :: thesis:
thus (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x) :: thesis:

proof

per cases ;

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

then Args (o,(product A)) = {{}} by PRALG_2:4;
then A24: x = {} by TARSKI:def 1;
then A25: (F . (the_result_sort_of o)) . (const (o,(product A))) in rng (F . (the_result_sort_of o)) by A21, A22, FUNCT_1:def 3;
reconsider g1 = (F . (the_result_sort_of o)) . (const (o,(product A))) as Function by A19;
A26: dom (const (o,(product A))) = I by PARTFUN1:def 2, A22, A24;

A27: now :: thesis:

let e be Element of Class EqR; :: thesis:
consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that
A28: Ji = (id (Class EqR)) . e and
A29: Cs = (A / EqR) . e and
A30: (product (A / EqR)) . e = product Cs by Def5;
A31: dom ((const (o,(product A))) | e) = I /\ e by A26, RELAT_1:61
.= e by XBOOLE_1:28 ;

A32: now :: thesis:

let i1 be object ; :: thesis:
A33: dom (A | e) = (dom A) /\ e by RELAT_1:61
.= I /\ e by PARTFUN1:def 2
.= e by XBOOLE_1:28 ;
assume A34: i1 in e ; :: thesis:
then reconsider ii = i1 as Element of Ji by A28;
reconsider ii9 = ii as Element of I by A34;
Cs = A | e by A29, Def4;
then A35: Cs . ii = A . ii9 by A34, A33, FUNCT_1:47;
thus ((const (o,(product A))) | e) . i1 = (const (o,(product A))) . i1 by A31, A34, FUNCT_1:47
.= const (o,(A . ii9)) by A23, Th9
.= (const (o,(product Cs))) . i1 by A23, A35, Th9 ; :: thesis:

end;

const (o,(product Cs)) in Funcs (Ji,(union { (Result (o,(Cs . i9))) where i9 is Element of Ji : verum } )) by A23, Th8;
then dom (const (o,(product Cs))) = e by A28, FUNCT_2:92;
hence (const (o,(product A))) | e = const (o,((product (A / EqR)) . e)) by A30, A31, A32, FUNCT_1:2; :: thesis:

end;

A36: const (o,(product A)) in the Sorts of (product A) . (the_result_sort_of o) by A17, A24, PRALG_2:3;

A37: now :: thesis:

let x1 be object ; :: thesis:
consider f1 being Function such that
A38: f1 = const (o,(product A)) ;
assume x1 in Class EqR ; :: thesis:
then reconsider e = x1 as Element of Class EqR ;
g1 . e = f1 | e by A20, A36, A38;
hence g1 . x1 = const (o,((product (A / EqR)) . e)) by A27, A38
.= (const (o,(product (product (A / EqR))))) . x1 by A23, Th9 ;
:: thesis:

end;

const (o,(product (product (A / EqR)))) in Funcs ((Class EqR),(union { (Result (o,((product (A / EqR)) . i9))) where i9 is Element of Class EqR : verum } )) by A23, Th8;
then A39: dom (const (o,(product (product (A / EqR))))) = Class EqR by FUNCT_2:92;
dom g1 = Class EqR by PARTFUN1:def 2, A19, A25;
then (F . (the_result_sort_of o)) . (const (o,(product A))) = const (o,(product (product (A / EqR)))) by A39, A37, FUNCT_1:2;
hence (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x) by A23, A24, Th11; :: thesis:

end;

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

A41: (Den (o,(product (product (A / EqR))))) . (F # x) in product (Carrier ((product (A / EqR)),(the_result_sort_of o))) by Th19;
then reconsider f1 = (Den (o,(product (product (A / EqR))))) . (F # x) as Function ;
A42: dom f1 = Class EqR by PARTFUN1:def 2, A41;
A43: (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) in rng (F . (the_result_sort_of o)) by A21, A22, FUNCT_1:def 3;
reconsider g1 = (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) as Function by A19;

A44: now :: thesis:

let e be Element of Class EqR; :: thesis:
consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that
A45: Ji = (id (Class EqR)) . e and
A46: Cs = (A / EqR) . e and
A47: (product (A / EqR)) . e = product Cs by Def5;
A48: (commute (F # x)) . e is Element of Args (o,((product (A / EqR)) . e)) by A40, Th20;
then A49: (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) in product (Carrier (Cs,(the_result_sort_of o))) by A47, Th19;
then reconsider f3 = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) as Function ;

A50: now :: thesis:

let i1 be Element of I; :: thesis:
assume A51: i1 in e ; :: thesis:
then reconsider i2 = i1 as Element of Ji by A45;

A52: now :: thesis:

let n be object ; :: thesis:
assume A53: 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 SortSymbol of S ;
A54: x . n in product (Carrier (A,((the_arity_of o) /. n))) by A53, Th15;
then reconsider f4 = x . n as Function ;
A55: x . n in product (Carrier (A,s1)) by A53, A54, PARTFUN1:def 6;
then A56: x . n in (SORTS A) . s1 by PRALG_2:def 10;
dom f4 = I by PARTFUN1:def 2, A55;
then A57: dom (f4 | e) = I /\ e by RELAT_1:61
.= e by XBOOLE_1:28 ;
(F # x) . n in product (Carrier ((product (A / EqR)),((the_arity_of o) /. n))) by A53, Th15;
then reconsider f5 = (F # x) . n as Function ;
consider f7 being Function of ( the Sorts of (product A) . s1),( the Sorts of (product (product (A / EqR))) . s1) such that
A58: f7 = F . s1 and
A59: for x9 being object st x9 in the Sorts of (product A) . s1 holds
S₁[f7 . x9,x9,s1] by A15;
f5 = (F . ((the_arity_of o) /. n)) . (x . n) by A53, Th13
.= f7 . (x . n) by A53, A58, PARTFUN1:def 6 ;
then A60: f5 . e = f4 | e by A56, A59;
then reconsider f6 = f5 . e as Function ;
f6 = ((commute (F # x)) . e) . n by A53, Th21;
hence ((commute ((commute (F # x)) . e)) . i1) . n = (f4 | e) . i2 by A47, A48, A53, A60, Th21
.= f4 . i2 by A51, A57, FUNCT_1:47
.= ((commute x) . i1) . n by A53, Th21 ;
:: thesis:

end;

(commute x) . i1 is Element of Args (o,(A . i1)) by A40, Th20;
then (commute x) . i1 in Args (o,(A . i1)) ;
then (commute x) . i1 in product ( the Sorts of (A . i1) * (the_arity_of o)) by PRALG_2:3;
then A61: dom ((commute x) . i1) = dom ( the Sorts of (A . i1) * (the_arity_of o)) by CARD_3:9
.= dom (the_arity_of o) by PRALG_2:3 ;
(commute ((commute (F # x)) . e)) . i2 is Element of Args (o,(Cs . i2)) by A40, A47, A48, Th20;
then (commute ((commute (F # x)) . e)) . i2 in Args (o,(Cs . i2)) ;
then (commute ((commute (F # x)) . e)) . i2 in product ( the Sorts of (Cs . i2) * (the_arity_of o)) by PRALG_2:3;
then dom ((commute ((commute (F # x)) . e)) . i1) = dom ( the Sorts of (Cs . i2) * (the_arity_of o)) by CARD_3:9
.= dom (the_arity_of o) by PRALG_2:3 ;
hence (commute ((commute (F # x)) . e)) . i1 = (commute x) . i1 by A61, A52; :: thesis:

end;

let f2 be Function; :: thesis:
assume A62: f2 = (Den (o,(product A))) . x ; :: thesis:
dom f2 = I by PARTFUN1:def 2, A22, A62;
then A63: dom (f2 | e) = I /\ e by RELAT_1:61
.= e by XBOOLE_1:28 ;
A64: (commute (F # x)) . e is Element of Args (o,(product Cs)) by A40, A47, Th20;

A65: now :: thesis:

let x1 be object ; :: thesis:
A66: dom (A | e) = (dom A) /\ e by RELAT_1:61
.= I /\ e by PARTFUN1:def 2
.= e by XBOOLE_1:28 ;
assume A67: x1 in e ; :: thesis:
then reconsider i2 = x1 as Element of Ji by A45;
reconsider i1 = i2 as Element of I by A67;
Cs = A | e by A46, Def4;
then Cs . i2 = A . i1 by A67, A66, FUNCT_1:47;
hence f3 . x1 = (Den (o,(A . i1))) . ((commute ((commute (F # x)) . e)) . i2) by A40, A47, A64, Th22
.= (Den (o,(A . i1))) . ((commute x) . i1) by A50, A67
.= f2 . x1 by A40, A62, Th22
.= (f2 | e) . x1 by A63, A67, FUNCT_1:47 ;
:: thesis:

end;

dom f3 = dom (Carrier (Cs,(the_result_sort_of o))) by A49, CARD_3:9
.= e by A45, PARTFUN1:def 2 ;
hence f2 | e = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) by A63, A65, FUNCT_1:2; :: thesis:

end;

A68: now :: thesis:

reconsider f2 = (Den (o,(product A))) . x as Function by A22;
let x1 be object ; :: thesis:
assume x1 in Class EqR ; :: thesis:
then reconsider e = x1 as Element of Class EqR ;
g1 . e = f2 | e by A20, A18;
hence g1 . x1 = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) by A44
.= f1 . x1 by A40, Th22 ;
:: thesis:

end;

dom g1 = Class EqR by PARTFUN1:def 2, A19, A43;
hence (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x) by A42, A68, FUNCT_1:2; :: thesis:

end;

F is "1-1"

proof

let s be set ; :: according to MSUALG_3:def 2 :: thesis:
let g be Function; :: thesis:
assume that
A69: s in dom F and
A70: F . s = g ; :: thesis:
consider f being Function of ( the Sorts of (product A) . s),( the Sorts of (product (product (A / EqR))) . s) such that
A71: f = F . s and
A72: for x being object st x in the Sorts of (product A) . s holds
S₁[f . x,x,s] by A15, A69;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A73: x1 in dom g and
A74: x2 in dom g and
A75: g . x1 = g . x2 ; :: thesis:
A76: dom f = dom g by A70, A71;
thus x1 = x2 :: thesis:

proof

reconsider s9 = s as SortSymbol of S by A69;
A77: the Sorts of (product A) . s9 = product (Carrier (A,s9)) by PRALG_2:def 10;
then A78: ex gg being Function st
( x1 = gg & dom gg = dom (Carrier (A,s9)) & ( for x9 being object st x9 in dom (Carrier (A,s9)) holds
gg . x9 in (Carrier (A,s9)) . x9 ) ) by A73, A76, CARD_3:def 5;
A79: ex gg1 being Function st
( x2 = gg1 & dom gg1 = dom (Carrier (A,s9)) & ( for x9 being object st x9 in dom (Carrier (A,s9)) holds
gg1 . x9 in (Carrier (A,s9)) . x9 ) ) by A74, A76, A77, CARD_3:def 5;
reconsider x2 = x2 as Function by A74, A76, A77;
A80: dom x2 = I by A79, PARTFUN1:def 2;
reconsider x1 = x1 as Function by A73, A76, A77;
A81: the Sorts of (product (product (A / EqR))) . s = product (Carrier ((product (A / EqR)),s9)) by PRALG_2:def 10;
A82: for i being object st i in I holds
x1 . i = x2 . i

proof

reconsider f99 = f . x2 as Function by A81;
let i be object ; :: thesis:
assume A83: i in I ; :: thesis:
then A84: Class (EqR,i) is Element of Class EqR by EQREL_1:def 3;
then x1 | (Class (EqR,i)) = f99 . (Class (EqR,i)) by A70, A73, A75, A71, A72, A76
.= x2 | (Class (EqR,i)) by A74, A72, A76, A84 ;
then x1 . i = (x2 | (Class (EqR,i))) . i by A83, EQREL_1:20, FUNCT_1:49
.= x2 . i by A83, EQREL_1:20, FUNCT_1:49 ;
hence x1 . i = x2 . i ; :: thesis:

end;

dom x1 = I by A78, PARTFUN1:def 2;
hence x1 = x2 by A80, A82, FUNCT_1:2; :: thesis:

end;

then A85: F is_monomorphism product A, product (product (A / EqR)) by A16;
F is "onto"

proof

let s be set ; :: according to MSUALG_3:def 3 :: thesis:
assume A86: s in the carrier of S ; :: thesis:
reconsider s9 = s as SortSymbol of S by A86;
consider f being Function of ( the Sorts of (product A) . s),( the Sorts of (product (product (A / EqR))) . s) such that
A87: f = F . s and
A88: for x being object st x in the Sorts of (product A) . s holds
S₁[f . x,x,s] by A15, A86;
A89: the Sorts of (product A) . s9 = product (Carrier (A,s9)) by PRALG_2:def 10;
for y being object holds
( y in the Sorts of (product (product (A / EqR))) . s iff ex x being object st
( x in dom f & y = f . x ) )

proof

let y be object ; :: thesis:
A90: ( y in the Sorts of (product (product (A / EqR))) . s implies ex x being set st
( x in dom f & y = f . x ) )

proof

assume y in the Sorts of (product (product (A / EqR))) . s ; :: thesis:
then A91: y in product (Carrier ((product (A / EqR)),s9)) by PRALG_2:def 10;
then A92: ex gg being Function st
( y = gg & dom gg = dom (Carrier ((product (A / EqR)),s9)) & ( for x9 being object st x9 in dom (Carrier ((product (A / EqR)),s9)) holds
gg . x9 in (Carrier ((product (A / EqR)),s9)) . x9 ) ) by CARD_3:def 5;
reconsider y = y as Function by A91;
defpred S₂[ object , object ] means ex e being Element of Class EqR ex f being Function st
( $1 in e & f = y . e & $2 = f . $1 );
A93: for i being object st i in I holds
ex j being object st S₂[i,j]

proof

let i be object ; :: thesis:
assume A94: i in I ; :: thesis:
Class (EqR,i) in Class EqR by A94, EQREL_1:def 3;
then consider e being Element of Class EqR such that
A95: e = Class (EqR,i) ;
consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that
Ji = (id (Class EqR)) . e and
Cs = (A / EqR) . e and
A96: (product (A / EqR)) . e = product Cs by Def5;
ex U0 being MSAlgebra over S st
( U0 = (product (A / EqR)) . e & (Carrier ((product (A / EqR)),s9)) . e = the Sorts of U0 . s9 ) by PRALG_2:def 9;
then ( dom (Carrier ((product (A / EqR)),s9)) = Class EqR & (Carrier ((product (A / EqR)),s9)) . e = product (Carrier (Cs,s9)) ) by A96, PARTFUN1:def 2, PRALG_2:def 10;
then reconsider y9 = y . e as Function by A92, Lm1;
S₂[i,y9 . i] by A94, A95, EQREL_1:20;
hence ex j being object st S₂[i,j] ; :: thesis:

end;

consider x being ManySortedSet of I such that
A97: for i being object st i in I holds
S₂[i,x . i] from PBOOLE:sch 3(A93);
A98: dom (Carrier ((product (A / EqR)),s9)) = Class EqR by PARTFUN1:def 2;
A99: for z being object st z in dom (Carrier (A,s9)) holds
x . z in (Carrier (A,s9)) . z

proof

let z be object ; :: thesis:
assume z in dom (Carrier (A,s9)) ; :: thesis:
then z in I ;
then consider e being Element of Class EqR, f1 being Function such that
A100: z in e and
A101: ( f1 = y . e & x . z = f1 . z ) by A97;
dom ((Carrier (A,s9)) | e) = (dom (Carrier (A,s9))) /\ e by RELAT_1:61
.= I /\ e by PARTFUN1:def 2
.= e by XBOOLE_1:28 ;
then A102: ((Carrier (A,s9)) | e) . z = (Carrier (A,s9)) . z by A100, FUNCT_1:47;
consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that
A103: Ji = (id (Class EqR)) . e and
A104: Cs = (A / EqR) . e and
A105: (product (A / EqR)) . e = product Cs by Def5;
( Cs = A | e & Ji = e ) by A103, A104, Def4;
then A106: Carrier (Cs,s9) = (Carrier (A,s9)) | e by Th2;
ex U0 being MSAlgebra over S st
( U0 = (product (A / EqR)) . e & (Carrier ((product (A / EqR)),s9)) . e = the Sorts of U0 . s9 ) by PRALG_2:def 9;
then A107: (Carrier ((product (A / EqR)),s9)) . e = product (Carrier (Cs,s9)) by A105, PRALG_2:def 10;
y . e in (Carrier ((product (A / EqR)),s9)) . e by A92, A98;
then A108: ex g being Function st
( y . e = g & dom g = dom (Carrier (Cs,s9)) & ( for x9 being object st x9 in dom (Carrier (Cs,s9)) holds
g . x9 in (Carrier (Cs,s9)) . x9 ) ) by A107, CARD_3:def 5;
dom (Carrier (Cs,s9)) = e by A103, PARTFUN1:def 2;
hence x . z in (Carrier (A,s9)) . z by A100, A101, A108, A102, A106; :: thesis:

end;

dom x = I by PARTFUN1:def 2
.= dom (Carrier (A,s9)) by PARTFUN1:def 2 ;
then A109: x in the Sorts of (product A) . s9 by A89, A99, CARD_3:9;
then A110: x in dom f by FUNCT_2:def 1;
then f . x in rng f by FUNCT_1:def 3;
then f . x in the Sorts of (product (product (A / EqR))) . s ;
then A111: f . x in product (Carrier ((product (A / EqR)),s9)) by PRALG_2:def 10;
then reconsider f9 = f . x as Function ;
A112: for e being object st e in Class EqR holds
y . e = f9 . e

proof

let e be object ; :: thesis:
assume e in Class EqR ; :: thesis:
then reconsider e = e as Element of Class EqR ;
consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that
A113: Ji = (id (Class EqR)) . e and
Cs = (A / EqR) . e and
A114: (product (A / EqR)) . e = product Cs by Def5;
ex U0 being MSAlgebra over S st
( U0 = (product (A / EqR)) . e & (Carrier ((product (A / EqR)),s9)) . e = the Sorts of U0 . s9 ) by PRALG_2:def 9;
then A115: (Carrier ((product (A / EqR)),s9)) . e = product (Carrier (Cs,s9)) by A114, PRALG_2:def 10;
A116: y . e in (Carrier ((product (A / EqR)),s9)) . e by A92, A98;
then reconsider y9 = y . e as Function by A115;
A117: dom (x | e) = (dom x) /\ e by RELAT_1:61
.= I /\ e by PARTFUN1:def 2
.= e by XBOOLE_1:28 ;
A118: for i being object st i in e holds
(x | e) . i = y9 . i

proof

let i be object ; :: thesis:
assume A119: i in e ; :: thesis:
then consider e1 being Element of Class EqR, f1 being Function such that
A120: i in e1 and
A121: ( f1 = y . e1 & x . i = f1 . i ) by A97;
e = e1 by A119, A120, Th3;
hence (x | e) . i = y9 . i by A117, A119, A121, FUNCT_1:47; :: thesis:

end;

ex g being Function st
( y . e = g & dom g = dom (Carrier (Cs,s9)) & ( for x9 being object st x9 in dom (Carrier (Cs,s9)) holds
g . x9 in (Carrier (Cs,s9)) . x9 ) ) by A116, A115, CARD_3:def 5;
then dom y9 = e by A113, PARTFUN1:def 2;
then x | e = y9 by A117, A118;
hence y . e = f9 . e by A88, A109; :: thesis:

end;

ex gg9 being Function st
( f . x = gg9 & dom gg9 = dom (Carrier ((product (A / EqR)),s9)) & ( for x9 being object st x9 in dom (Carrier ((product (A / EqR)),s9)) holds
gg9 . x9 in (Carrier ((product (A / EqR)),s9)) . x9 ) ) by A111, CARD_3:def 5;
then y = f9 by A92, A112;
hence ex x being set st
( x in dom f & y = f . x ) by A110; :: thesis:

end;

( ex x being set st
( x in dom f & y = f . x ) implies y in the Sorts of (product (product (A / EqR))) . s )

proof

given x being set such that A122: x in dom f and
A123: y = f . x ; :: thesis:
f . x in rng f by A122, FUNCT_1:def 3;
hence y in the Sorts of (product (product (A / EqR))) . s by A123; :: thesis:

end;

hence ( y in the Sorts of (product (product (A / EqR))) . s iff ex x being object st
( x in dom f & y = f . x ) ) by A90; :: thesis:

end;

hence rng (F . s) = the Sorts of (product (product (A / EqR))) . s by A87, FUNCT_1:def 3; :: thesis:

end;

then F is_epimorphism product A, product (product (A / EqR)) by A16;
then F is_isomorphism product A, product (product (A / EqR)) by A85;
hence product A, product (product (A / EqR)) are_isomorphic ; :: thesis: