set Ob3 = [:the carrier of C,the carrier of C,the carrier of C:];
set G = the_hom_sets_of C;
deffunc H₁( set ) -> Element of bool [:[:the U4 of C,the U4 of C:],the U4 of C:] = the Comp of C | [:((the_hom_sets_of C) . (($1 `1 ) `2 ),($1 `2 )),((the_hom_sets_of C) . (($1 `1 ) `1 ),(($1 `1 ) `2 )):];
consider o being Function such that
A1: dom o = [:the carrier of C,the carrier of C,the carrier of C:] and
A2: for e being set st e in [:the carrier of C,the carrier of C,the carrier of C:] holds
o . e = H₁(e) from FUNCT_1:sch 3();
reconsider o = o as ManySortedSet of by A1, PARTFUN1:def 4, RELAT_1:def 18;

now

let e be set ; :: thesis: ( e in dom o implies o . e is Function )
assume e in dom o ; :: thesis: o . e is Function
then o . e = the Comp of C | [:((the_hom_sets_of C) . ((e `1 ) `2 ),(e `2 )),((the_hom_sets_of C) . ((e `1 ) `1 ),((e `1 ) `2 )):] by A1, A2;
hence o . e is Function ; :: thesis: verum

end;

then reconsider o = o as ManySortedFunction of by FUNCOP_1:def 6;

now

let e be set ; :: thesis: ( e in [:the carrier of C,the carrier of C,the carrier of C:] implies o . e is Function of ({|(the_hom_sets_of C),(the_hom_sets_of C)|} . e),({|(the_hom_sets_of C)|} . e) )
assume A3: e in [:the carrier of C,the carrier of C,the carrier of C:] ; :: thesis: o . e is Function of ({|(the_hom_sets_of C),(the_hom_sets_of C)|} . e),({|(the_hom_sets_of C)|} . e)
reconsider f = o . e as Function ;
consider i, j, k being Object of C such that
A4: e = [i,j,k] by A3, DOMAIN_1:15;
reconsider e' = e as Element of [:the carrier of C,the carrier of C,the carrier of C:] by A3;
A5: ([i,j,k] `1 ) `1 = e' `1 by A4, MCART_1:50
.= i by A4, MCART_1:47 ;
A6: ([i,j,k] `1 ) `2 = e' `2 by A4, MCART_1:50
.= j by A4, MCART_1:47 ;
A7: [i,j,k] `2 = e' `3 by A4, MCART_1:50
.= k by A4, MCART_1:47 ;
A8: ( (the_hom_sets_of C) . i,j = Hom i,j & (the_hom_sets_of C) . j,k = Hom j,k ) by Def3;
A9: f = the Comp of C | [:((the_hom_sets_of C) . j,k),((the_hom_sets_of C) . i,j):] by A2, A4, A5, A6, A7;
A10: {|(the_hom_sets_of C)|} . e = {|(the_hom_sets_of C)|} . i,j,k by A4, MULTOP_1:def 1
.= (the_hom_sets_of C) . i,k by ALTCAT_1:def 5
.= Hom i,k by Def3 ;
A11: {|(the_hom_sets_of C),(the_hom_sets_of C)|} . e = {|(the_hom_sets_of C),(the_hom_sets_of C)|} . i,j,k by A4, MULTOP_1:def 1
.= [:(Hom j,k),(Hom i,j):] by A8, ALTCAT_1:def 6 ;

A12: now

assume {|(the_hom_sets_of C)|} . e = {} ; :: thesis: {|(the_hom_sets_of C),(the_hom_sets_of C)|} . e = {}
then ( Hom i,j = {} or Hom j,k = {} ) by A10, CAT_1:52;
hence {|(the_hom_sets_of C),(the_hom_sets_of C)|} . e = {} by A11, ZFMISC_1:113; :: thesis: verum

end;

[:(Hom j,k),(Hom i,j):] c= dom the Comp of C by Th11;
then A13: dom f = {|(the_hom_sets_of C),(the_hom_sets_of C)|} . e by A8, A9, A11, RELAT_1:91;
the Comp of C .: [:(Hom j,k),(Hom i,j):] c= Hom i,k by Th12;
then rng f c= {|(the_hom_sets_of C)|} . e by A8, A9, A10, RELAT_1:148;
hence o . e is Function of ({|(the_hom_sets_of C),(the_hom_sets_of C)|} . e),({|(the_hom_sets_of C)|} . e) by A12, A13, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum

end;

then reconsider o = o as BinComp of (the_hom_sets_of C) by PBOOLE:def 18;
take o ; :: thesis: for i, j, k being Object of C holds o . i,j,k = the Comp of C | [:((the_hom_sets_of C) . j,k),((the_hom_sets_of C) . i,j):]
let i, j, k be Object of C; :: thesis: o . i,j,k = the Comp of C | [:((the_hom_sets_of C) . j,k),((the_hom_sets_of C) . i,j):]
reconsider e = [i,j,k] as Element of [:the carrier of C,the carrier of C,the carrier of C:] ;
A14: ([i,j,k] `1 ) `1 = e `1 by MCART_1:50
.= i by MCART_1:47 ;
A15: ([i,j,k] `1 ) `2 = e `2 by MCART_1:50
.= j by MCART_1:47 ;
A16: [i,j,k] `2 = e `3 by MCART_1:50
.= k by MCART_1:47 ;
thus o . i,j,k = o . [i,j,k] by MULTOP_1:def 1
.= the Comp of C | [:((the_hom_sets_of C) . j,k),((the_hom_sets_of C) . i,j):] by A2, A14, A15, A16 ; :: thesis: verum