defpred S₁[ set , set ] means ( ( $1 `1 = 1 & ex a being Element of F₁() st
( $1 = idsym a & ex F being Function of {{}},F₃(a,a) st
( F = $2 & F . {} = F₅(a) ) ) ) or ( $1 `1 = 2 & ex a, b, c being Element of F₁() st
( $1 = compsym (a,b,c) & ex F being Function of (product <*F₃(b,c),F₃(a,b)*>),F₃(a,c) st
( F = $2 & ( for f, g being set st f in F₃(a,b) & g in F₃(b,c) holds
F . <*g,f*> = F₄(a,b,c,g,f) ) ) ) ) );
set CS = CatSign F₁();
A4: for o being set st o in the carrier' of (CatSign F₁()) holds
ex u being set st S₁[o,u]

let o be set ; :: thesis:
assume A5: o in the carrier' of (CatSign F₁()) ; :: thesis:

A6: now

assume o `1 = 1 ; :: thesis:
then consider a being Element of F₁() such that
A7: o = idsym a by A5, Th26;
set F = {} :-> F₅(a);
reconsider u = {} :-> F₅(a) as set ;
take u = u; :: thesis:
take a = a; :: thesis:
thus o = idsym a by A7; :: thesis:
F₅(a) in F₃(a,a) by A2;
then {F₅(a)} c= F₃(a,a) by ZFMISC_1:37;
then ( dom ({} :-> F₅(a)) = {{}} & rng ({} :-> F₅(a)) c= F₃(a,a) ) by FUNCOP_1:19, XBOOLE_1:1;
then reconsider F = {} :-> F₅(a) as Function of {{}},F₃(a,a) by FUNCT_2:4;
take F = F; :: thesis:
{} in {{}} by TARSKI:def 1;
hence ( F = u & F . {} = F₅(a) ) by FUNCOP_1:13; :: thesis:

end;

A8: now

assume o `1 = 2 ; :: thesis:
then consider a, b, c being Element of F₁() such that
A9: o = compsym (a,b,c) by A5, Th27;
defpred S₂[ set , set ] means ex f, g being set st
( f in F₃(a,b) & g in F₃(b,c) & $1 = <*g,f*> & $2 = F₄(a,b,c,g,f) );

A10: now

let x be set ; :: thesis:
assume x in product <*F₃(b,c),F₃(a,b)*> ; :: thesis:
then consider g, f being set such that
A11: ( g in F₃(b,c) & f in F₃(a,b) ) and
A12: x = <*g,f*> by FUNCT_6:2;
take u = F₄(a,b,c,g,f); :: thesis:
( F₃(a,b) c= F₂() & F₃(b,c) c= F₂() ) by A1;
hence u in F₃(a,c) by A3, A11; :: thesis:
thus S₂[x,u] by A11, A12; :: thesis:

end;

consider F being Function such that
A13: ( dom F = product <*F₃(b,c),F₃(a,b)*> & rng F c= F₃(a,c) ) and
A14: for x being set st x in product <*F₃(b,c),F₃(a,b)*> holds
S₂[x,F . x] from WELLORD2:sch 1(A10);
reconsider u = F as set ;
take u = u; :: thesis:
take a = a; :: thesis:
take b = b; :: thesis:
take c = c; :: thesis:
thus o = compsym (a,b,c) by A9; :: thesis:
reconsider F = F as Function of (product <*F₃(b,c),F₃(a,b)*>),F₃(a,c) by A13, FUNCT_2:4;
take F = F; :: thesis:
thus F = u ; :: thesis:
let f, g be set ; :: thesis:
assume ( f in F₃(a,b) & g in F₃(b,c) ) ; :: thesis:
then <*g,f*> in product <*F₃(b,c),F₃(a,b)*> by FUNCT_6:2;
then consider f9, g9 being set such that
f9 in F₃(a,b) and
g9 in F₃(b,c) and
A15: <*g,f*> = <*g9,f9*> and
A16: F . <*g,f*> = F₄(a,b,c,g9,f9) by A14;
A17: ( <*g,f*> . 1 = g & <*g,f*> . 2 = f ) by FINSEQ_1:61;
<*g,f*> . 1 = g9 by A15, FINSEQ_1:61;
hence F . <*g,f*> = F₄(a,b,c,g,f) by A15, A16, A17, FINSEQ_1:61; :: thesis:

end;

( o `1 = 1 or o `1 = 2 ) by A5, Th25;
hence ex u being set st S₁[o,u] by A6, A8; :: thesis:

end;

consider O being Function such that
A18: dom O = the carrier' of (CatSign F₁()) and
A19: for o being set st o in the carrier' of (CatSign F₁()) holds
S₁[o,O . o] from CLASSES1:sch 1(A4);
reconsider O = O as ManySortedSet of the carrier' of (CatSign F₁()) by A18, PARTFUN1:def 4, RELAT_1:def 18;
defpred S₂[ set , set ] means ex a, b being Element of F₁() st
( $1 = homsym (a,b) & $2 = F₃(a,b) );

A20: now

let s be set ; :: thesis:
assume s in the carrier of (CatSign F₁()) ; :: thesis:
then consider a, b being Element of F₁() such that
A21: s = homsym (a,b) by Th24;
take u = F₃(a,b); :: thesis:
thus S₂[s,u] by A21; :: thesis:

end;

consider S being Function such that
A22: dom S = the carrier of (CatSign F₁()) and
A23: for s being set st s in the carrier of (CatSign F₁()) holds
S₂[s,S . s] from CLASSES1:sch 1(A20);
reconsider S = S as ManySortedSet of the carrier of (CatSign F₁()) by A22, PARTFUN1:def 4, RELAT_1:def 18;
O is ManySortedFunction of (S #) * the Arity of (CatSign F₁()),S * the ResultSort of (CatSign F₁())

proof

let o be set ; :: according to PBOOLE:def 18 :: thesis:
assume o in the carrier' of (CatSign F₁()) ; :: thesis:
then reconsider o = o as OperSymbol of (CatSign F₁()) ;
A24: ((S #) * the Arity of (CatSign F₁())) . o = (S #) . (the_arity_of o) by FUNCT_2:21
.= product (S * (the_arity_of o)) by PBOOLE:def 19 ;
A25: (S * the ResultSort of (CatSign F₁())) . o = S . (the_result_sort_of o) by FUNCT_2:21;

per cases by Th25;

suppose ( o `1 = 1 & 1 <> 2 ) ; :: thesis:

then consider a being Element of F₁() such that
A26: ( o = idsym a & ex F being Function of {{}},F₃(a,a) st
( F = O . o & F . {} = F₅(a) ) ) by A19;
A27: ( the_arity_of (idsym a) = {} & {} = S * {} ) by Def5;
A28: the_result_sort_of (idsym a) = homsym (a,a) by Def5;
consider c, b being Element of F₁() such that
A29: homsym (a,a) = homsym (c,b) and
A30: S . (homsym (a,a)) = F₃(c,b) by A23;
( a = b & a = c ) by A29, Th22;
hence O . o is Element of bool [:(((S #) * the Arity of (CatSign F₁())) . o),((S * the ResultSort of (CatSign F₁())) . o):] by A24, A25, A26, A30, A27, A28, CARD_3:19; :: thesis:

end;

suppose ( o `1 = 2 & 1 <> 2 ) ; :: thesis:

then consider a, b, c being Element of F₁() such that
A31: o = compsym (a,b,c) and
A32: ex F being Function of (product <*F₃(b,c),F₃(a,b)*>),F₃(a,c) st
( F = O . o & ( for f, g being set st f in F₃(a,b) & g in F₃(b,c) holds
F . <*g,f*> = F₄(a,b,c,g,f) ) ) by A19;
A33: the_result_sort_of (compsym (a,b,c)) = homsym (a,c) by Def5;
consider ax, cx being Element of F₁() such that
A34: homsym (a,c) = homsym (ax,cx) and
A35: S . (homsym (a,c)) = F₃(ax,cx) by A23;
( ax = a & cx = c ) by A34, Th22;
then A36: (S * the ResultSort of (CatSign F₁())) . o = F₃(a,c) by A31, A35, A33, FUNCT_2:21;
A37: the_arity_of (compsym (a,b,c)) = <*(homsym (b,c)),(homsym (a,b))*> by Def5;
consider a9, b9 being Element of F₁() such that
A38: homsym (a,b) = homsym (a9,b9) and
A39: S . (homsym (a,b)) = F₃(a9,b9) by A23;
consider b99, c9 being Element of F₁() such that
A40: homsym (b,c) = homsym (b99,c9) and
A41: S . (homsym (b,c)) = F₃(b99,c9) by A23;
A42: ( b99 = b & c9 = c ) by A40, Th22;
( a9 = a & b9 = b ) by A38, Th22;
then ((S #) * the Arity of (CatSign F₁())) . o = product <*F₃(b,c),F₃(a,b)*> by A22, A24, A31, A39, A41, A42, A37, FINSEQ_2:145;
hence O . o is Element of bool [:(((S #) * the Arity of (CatSign F₁())) . o),((S * the ResultSort of (CatSign F₁())) . o):] by A32, A36; :: thesis:

end;

then reconsider O = O as ManySortedFunction of (S #) * the Arity of (CatSign F₁()),S * the ResultSort of (CatSign F₁()) ;
take A = MSAlgebra(# S,O #); :: thesis:

hereby :: thesis:

let a, b be Element of F₁(); :: thesis:
consider a9, b9 being Element of F₁() such that
A43: homsym (a,b) = homsym (a9,b9) and
A44: S . (homsym (a,b)) = F₃(a9,b9) by A23;
a = a9 by A43, Th22;
hence the Sorts of A . (homsym (a,b)) = F₃(a,b) by A43, A44, Th22; :: thesis:

end;

hereby :: thesis:

let a be Element of F₁(); :: thesis:
(idsym a) `1 = 1 by MCART_1:7;
then ex b being Element of F₁() st
( idsym a = idsym b & ex F being Function of {{}},F₃(b,b) st
( F = O . (idsym a) & F . {} = F₅(b) ) ) by A19;
hence (Den ((idsym a),A)) . {} = F₅(a) by Th21; :: thesis:

end;

let a, b, c be Element of F₁(); :: thesis:
set o = compsym (a,b,c);
(compsym (a,b,c)) `1 = 2 by MCART_1:7;
then consider a9, b9, c9 being Element of F₁() such that
A45: compsym (a,b,c) = compsym (a9,b9,c9) and
A46: ex F being Function of (product <*F₃(b9,c9),F₃(a9,b9)*>),F₃(a9,c9) st
( F = O . (compsym (a,b,c)) & ( for f, g being set st f in F₃(a9,b9) & g in F₃(b9,c9) holds
F . <*g,f*> = F₄(a9,b9,c9,g,f) ) ) by A19;
A47: c = c9 by A45, Th23;
let f, g be Element of F₂(); :: thesis:
assume A48: ( f in F₃(a,b) & g in F₃(b,c) ) ; :: thesis:
( a = a9 & b = b9 ) by A45, Th23;
hence (Den ((compsym (a,b,c)),A)) . <*g,f*> = F₄(a,b,c,g,f) by A46, A47, A48; :: thesis: