defpred S₁[ object , object ] 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 object st o in the carrier' of (CatSign F₁()) holds
ex u being object st S₁[o,u]

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

assume o `1 = 1 ; :: thesis:
then consider a being Element of F₁() such that
A7: o = idsym a by A5, Th17;
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:31;
then ( dom ({} :-> F₅(a)) = {{}} & rng ({} :-> F₅(a)) c= F₃(a,a) ) ;
then reconsider F = {} :-> F₅(a) as Function of {{}},F₃(a,a) by FUNCT_2:2;
take F = F; :: thesis:
{} in {{}} by TARSKI:def 1;
hence ( F = u & F . {} = F₅(a) ) by FUNCOP_1:7; :: thesis:

end;

A8: now :: thesis:

assume o `1 = 2 ; :: thesis:
then consider a, b, c being Element of F₁() such that
A9: o = compsym (a,b,c) by A5, Th18;
defpred S₂[ object , object ] 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 :: thesis:

let x be object ; :: thesis:
assume x in product <*F₃(b,c),F₃(a,b)*> ; :: thesis:
then consider g, f being object such that
A11: ( g in F₃(b,c) & f in F₃(a,b) ) and
A12: x = <*g,f*> by FINSEQ_3:124;
reconsider u = F₄(a,b,c,g,f) as object ;
take u = u; :: 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 object st x in product <*F₃(b,c),F₃(a,b)*> holds
S₂[x,F . x] from FUNCT_1:sch 6(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:2;
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 FINSEQ_3:124;
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 ) ;
<*g,f*> . 1 = g9 by A15, FINSEQ_1:44;
hence F . <*g,f*> = F₄(a,b,c,g,f) by A15, A16, A17, FINSEQ_1:44; :: thesis:

end;

( o `1 = 1 or o `1 = 2 ) by A5, Th16;
hence ex u being object 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 object 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 2, RELAT_1:def 18;
defpred S₂[ object , object ] means ex a, b being Element of F₁() st
( $1 = homsym (a,b) & $2 = F₃(a,b) );

A20: now :: thesis:

let s be object ; :: 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 Th15;
reconsider u = F₃(a,b) as object ;
take u = u; :: 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 object 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 2, RELAT_1:def 18;
O is ManySortedFunction of (S #) * the Arity of (CatSign F₁()),S * the ResultSort of (CatSign F₁())

proof

let o be object ; :: according to PBOOLE:def 15 :: 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:15
.= product (S * (the_arity_of o)) by FINSEQ_2:def 5 ;
A25: (S * the ResultSort of (CatSign F₁())) . o = S . (the_result_sort_of o) by FUNCT_2:15;

per cases by Th16;

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 Def3;
A28: the_result_sort_of (idsym a) = homsym (a,a) by Def3;
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, Th13;
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:10; :: 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 Def3;
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, Th13;
then A36: (S * the ResultSort of (CatSign F₁())) . o = F₃(a,c) by A31, A35, A33, FUNCT_2:15;
A37: the_arity_of (compsym (a,b,c)) = <*(homsym (b,c)),(homsym (a,b))*> by Def3;
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, Th13;
( a9 = a & b9 = b ) by A38, Th13;
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:125;
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, Th13;
hence the Sorts of A . (homsym (a,b)) = F₃(a,b) by A43, A44, Th13; :: thesis:

end;

hereby :: thesis:

let a be Element of F₁(); :: thesis:
(idsym a) `1 = 1 ;
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 Th12; :: thesis:

end;

let a, b, c be Element of F₁(); :: thesis:
set o = compsym (a,b,c);
(compsym (a,b,c)) `1 = 2 ;
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, Th14;
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, Th14;
hence (Den ((compsym (a,b,c)),A)) . <*g,f*> = F₄(a,b,c,g,f) by A46, A47, A48; :: thesis: