deffunc H_{1}( object ) -> Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' 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))):];

set Ob3 = [: the carrier of C, the carrier of C, the carrier of C:];

set G = the_hom_sets_of C;

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 object st e in [: the carrier of C, the carrier of C, the carrier of C:] holds

o . e = H_{1}(e)
from FUNCT_1:sch 3();

reconsider o = o as ManySortedSet of [: the carrier of C, the carrier of C, the carrier of C:] by A1, PARTFUN1:def 2, RELAT_1: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:] ;

A12: ([i,j,k] `1) `1 = e `1_3

.= i by MCART_1:def 5 ;

A13: ([i,j,k] `1) `2 = e `2_3

.= j by MCART_1:def 6 ;

A14: [i,j,k] `2 = e `3_3

.= k by MCART_1:def 7 ;

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, A12, A13, A14 ; :: thesis: verum

set Ob3 = [: the carrier of C, the carrier of C, the carrier of C:];

set G = the_hom_sets_of C;

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 object st e in [: the carrier of C, the carrier of C, the carrier of C:] holds

o . e = H

reconsider o = o as ManySortedSet of [: the carrier of C, the carrier of C, the carrier of C:] by A1, PARTFUN1:def 2, RELAT_1:def 18;

now :: thesis: for e being object st e in dom o holds

o . e is Function

then reconsider o = o as ManySortedFunction of [: the carrier of C, the carrier of C, the carrier of C:] by FUNCOP_1:def 6;o . e is Function

let e be object ; :: 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;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

now :: thesis: for e being object st e in [: the carrier of C, the carrier of C, the carrier of C:] holds

o . e is Function of ({|(the_hom_sets_of C),(the_hom_sets_of C)|} . e),({|(the_hom_sets_of C)|} . e)

then reconsider o = o as BinComp of (the_hom_sets_of C) by PBOOLE:def 15;o . e is Function of ({|(the_hom_sets_of C),(the_hom_sets_of C)|} . e),({|(the_hom_sets_of C)|} . e)

let e be object ; :: 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) )

reconsider f = o . e as Function ;

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)

then consider i, j, k being Object of C such that

A4: e = [i,j,k] by DOMAIN_1:3;

reconsider e9 = e as Element of [: the carrier of C, the carrier of C, the carrier of C:] by A3;

A5: ([i,j,k] `1) `2 = e9 `2_3 by A4

.= j by A4, MCART_1:def 6 ;

A6: [i,j,k] `2 = e9 `3_3 by A4

.= k by A4, MCART_1:def 7 ;

([i,j,k] `1) `1 = e9 `1_3 by A4

.= i by A4, MCART_1:def 5 ;

then A7: f = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] by A2, A4, A5, A6;

A8: ( (the_hom_sets_of C) . (i,j) = Hom (i,j) & (the_hom_sets_of C) . (j,k) = Hom (j,k) ) by Def3;

A9: {|(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 3

.= Hom (i,k) by Def3 ;

A10: {|(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 4 ;

the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k) by Th11;

then A11: rng f c= {|(the_hom_sets_of C)|} . e by A8, A7, A9, RELAT_1:115;

[:(Hom (j,k)),(Hom (i,j)):] c= dom the Comp of C by Th10;

then dom f = {|(the_hom_sets_of C),(the_hom_sets_of C)|} . e by A8, A7, A10, RELAT_1:62;

hence o . e is Function of ({|(the_hom_sets_of C),(the_hom_sets_of C)|} . e),({|(the_hom_sets_of C)|} . e) by A11, FUNCT_2:2; :: thesis: verum

end;reconsider f = o . e as Function ;

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)

then consider i, j, k being Object of C such that

A4: e = [i,j,k] by DOMAIN_1:3;

reconsider e9 = e as Element of [: the carrier of C, the carrier of C, the carrier of C:] by A3;

A5: ([i,j,k] `1) `2 = e9 `2_3 by A4

.= j by A4, MCART_1:def 6 ;

A6: [i,j,k] `2 = e9 `3_3 by A4

.= k by A4, MCART_1:def 7 ;

([i,j,k] `1) `1 = e9 `1_3 by A4

.= i by A4, MCART_1:def 5 ;

then A7: f = the Comp of C | [:((the_hom_sets_of C) . (j,k)),((the_hom_sets_of C) . (i,j)):] by A2, A4, A5, A6;

A8: ( (the_hom_sets_of C) . (i,j) = Hom (i,j) & (the_hom_sets_of C) . (j,k) = Hom (j,k) ) by Def3;

A9: {|(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 3

.= Hom (i,k) by Def3 ;

A10: {|(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 4 ;

the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k) by Th11;

then A11: rng f c= {|(the_hom_sets_of C)|} . e by A8, A7, A9, RELAT_1:115;

[:(Hom (j,k)),(Hom (i,j)):] c= dom the Comp of C by Th10;

then dom f = {|(the_hom_sets_of C),(the_hom_sets_of C)|} . e by A8, A7, A10, RELAT_1:62;

hence o . e is Function of ({|(the_hom_sets_of C),(the_hom_sets_of C)|} . e),({|(the_hom_sets_of C)|} . e) by A11, FUNCT_2:2; :: thesis: verum

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:] ;

A12: ([i,j,k] `1) `1 = e `1_3

.= i by MCART_1:def 5 ;

A13: ([i,j,k] `1) `2 = e `2_3

.= j by MCART_1:def 6 ;

A14: [i,j,k] `2 = e `3_3

.= k by MCART_1:def 7 ;

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, A12, A13, A14 ; :: thesis: verum