deffunc H1( object ) -> Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] = the Comp of C | [:(() . (((\$1 `1) `2),(\$1 `2))),(() . (((\$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 = H1(e) from reconsider o = o as ManySortedSet of [: the carrier of C, the carrier of C, the carrier of C:] by ;
now :: thesis: for e being object st e in dom o holds
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 | [:(() . (((e `1) `2),(e `2))),(() . (((e `1) `1),((e `1) `2))):] by A1, A2;
hence o . e is Function ; :: thesis: verum
end;
then reconsider o = o as ManySortedFunction of [: the carrier of C, the carrier of C, the carrier of C:] by FUNCOP_1:def 6;
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 ({|(),()|} . e),( . 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 ({|(),()|} . e),( . 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 ({|(),()|} . e),( . 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 ;
A6: [i,j,k] `2 = e9 `3_3 by A4
.= k by ;
([i,j,k] `1) `1 = e9 `1_3 by A4
.= i by ;
then A7: f = the Comp of C | [:(() . (j,k)),(() . (i,j)):] by A2, A4, A5, A6;
A8: ( (the_hom_sets_of C) . (i,j) = Hom (i,j) & () . (j,k) = Hom (j,k) ) by Def3;
A9: . e = . (i,j,k) by
.= () . (i,k) by ALTCAT_1:def 3
.= Hom (i,k) by Def3 ;
A10: {|(),()|} . e = {|(),()|} . (i,j,k) by
.= [:(Hom (j,k)),(Hom (i,j)):] by ;
the Comp of C .: [:(Hom (j,k)),(Hom (i,j)):] c= Hom (i,k) by Th11;
then A11: rng f c= . e by ;
[:(Hom (j,k)),(Hom (i,j)):] c= dom the Comp of C by Th10;
then dom f = {|(),()|} . e by ;
hence o . e is Function of ({|(),()|} . e),( . e) by ; :: thesis: verum
end;
then reconsider o = o as BinComp of () by PBOOLE:def 15;
take o ; :: thesis: for i, j, k being Object of C holds o . (i,j,k) = the Comp of C | [:(() . (j,k)),(() . (i,j)):]
let i, j, k be Object of C; :: thesis: o . (i,j,k) = the Comp of C | [:(() . (j,k)),(() . (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 | [:(() . (j,k)),(() . (i,j)):] by A2, A12, A13, A14 ; :: thesis: verum