deffunc H_{1}( set , set , set ) -> set = FuncComp (F_{2}($1,$2),F_{2}($2,$3));

consider M being ManySortedSet of [:F_{1}(),F_{1}():] such that

A2: for i, j being Element of F_{1}() holds M . (i,j) = F_{2}(i,j)
from ALTCAT_1:sch 2();

consider c being ManySortedSet of [:F_{1}(),F_{1}(),F_{1}():] such that

A3: for i, j, k being Element of F_{1}() holds c . (i,j,k) = H_{1}(i,j,k)
from ALTCAT_1:sch 4();

c is Function-yielding_{1}(),F_{1}(),F_{1}():] ;

set C = AltCatStr(# F_{1}(),M,c #);

take AltCatStr(# F_{1}(),M,c #)
; :: thesis: ( the carrier of AltCatStr(# F_{1}(),M,c #) = F_{1}() & ( for i, j being Element of F_{1}() holds

( the Arrows of AltCatStr(# F_{1}(),M,c #) . (i,j) = F_{2}(i,j) & ( for i, j, k being Element of F_{1}() holds the Comp of AltCatStr(# F_{1}(),M,c #) . (i,j,k) = FuncComp (F_{2}(i,j),F_{2}(j,k)) ) ) ) )

thus the carrier of AltCatStr(# F_{1}(),M,c #) = F_{1}()
; :: thesis: for i, j being Element of F_{1}() holds

( the Arrows of AltCatStr(# F_{1}(),M,c #) . (i,j) = F_{2}(i,j) & ( for i, j, k being Element of F_{1}() holds the Comp of AltCatStr(# F_{1}(),M,c #) . (i,j,k) = FuncComp (F_{2}(i,j),F_{2}(j,k)) ) )

let i, j be Element of F_{1}(); :: thesis: ( the Arrows of AltCatStr(# F_{1}(),M,c #) . (i,j) = F_{2}(i,j) & ( for i, j, k being Element of F_{1}() holds the Comp of AltCatStr(# F_{1}(),M,c #) . (i,j,k) = FuncComp (F_{2}(i,j),F_{2}(j,k)) ) )

thus the Arrows of AltCatStr(# F_{1}(),M,c #) . (i,j) = F_{2}(i,j)
by A2; :: thesis: for i, j, k being Element of F_{1}() holds the Comp of AltCatStr(# F_{1}(),M,c #) . (i,j,k) = FuncComp (F_{2}(i,j),F_{2}(j,k))

let i, j, k be Element of F_{1}(); :: thesis: the Comp of AltCatStr(# F_{1}(),M,c #) . (i,j,k) = FuncComp (F_{2}(i,j),F_{2}(j,k))

thus the Comp of AltCatStr(# F_{1}(),M,c #) . (i,j,k) = FuncComp (F_{2}(i,j),F_{2}(j,k))
by A3; :: thesis: verum

consider M being ManySortedSet of [:F

A2: for i, j being Element of F

consider c being ManySortedSet of [:F

A3: for i, j, k being Element of F

c is Function-yielding

proof

then reconsider c = c as ManySortedFunction of [:F
let i be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not i in dom c or c . i is set )

assume i in dom c ; :: thesis: c . i is set

then i in [:F_{1}(),F_{1}(),F_{1}():]
;

then consider x1, x2, x3 being object such that

A4: ( x1 in F_{1}() & x2 in F_{1}() & x3 in F_{1}() )
and

A5: i = [x1,x2,x3] by MCART_1:68;

c . i = c . (x1,x2,x3) by A5, MULTOP_1:def 1

.= FuncComp (F_{2}(x1,x2),F_{2}(x2,x3))
by A3, A4
;

hence c . i is set ; :: thesis: verum

end;assume i in dom c ; :: thesis: c . i is set

then i in [:F

then consider x1, x2, x3 being object such that

A4: ( x1 in F

A5: i = [x1,x2,x3] by MCART_1:68;

c . i = c . (x1,x2,x3) by A5, MULTOP_1:def 1

.= FuncComp (F

hence c . i is set ; :: thesis: verum

now :: thesis: for i being object st i in [:F_{1}(),F_{1}(),F_{1}():] holds

c . i is Function of ({|M,M|} . i),({|M|} . i)

then reconsider c = c as BinComp of M by PBOOLE:def 15;c . i is Function of ({|M,M|} . i),({|M|} . i)

let i be object ; :: thesis: ( i in [:F_{1}(),F_{1}(),F_{1}():] implies c . i is Function of ({|M,M|} . i),({|M|} . i) )

assume i in [:F_{1}(),F_{1}(),F_{1}():]
; :: thesis: c . i is Function of ({|M,M|} . i),({|M|} . i)

then consider x1, x2, x3 being object such that

A6: x1 in F_{1}()
and

A7: x2 in F_{1}()
and

A8: x3 in F_{1}()
and

A9: i = [x1,x2,x3] by MCART_1:68;

M . (x1,x2) = F_{2}(x1,x2)
by A2, A6, A7;

then A10: [:F_{2}(x2,x3),F_{2}(x1,x2):] =
[:(M . (x2,x3)),(M . (x1,x2)):]
by A2, A7, A8

.= {|M,M|} . (x1,x2,x3) by A6, A7, A8, ALTCAT_1:def 4

.= {|M,M|} . i by A9, MULTOP_1:def 1 ;

A11: {|M|} . i = {|M|} . (x1,x2,x3) by A9, MULTOP_1:def 1

.= M . (x1,x3) by A6, A7, A8, ALTCAT_1:def 3 ;

.= FuncComp (F_{2}(x1,x2),F_{2}(x2,x3))
by A3, A6, A7, A8
;

then reconsider ci = c . i as Function ;

A17: dom ci = [:F_{2}(x2,x3),F_{2}(x1,x2):]
by A16, PARTFUN1:def 2;

rng (FuncComp (F_{2}(x1,x2),F_{2}(x2,x3))) c= F_{2}(x1,x3)

hence c . i is Function of ({|M,M|} . i),({|M|} . i) by A17, A10, A12, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

end;assume i in [:F

then consider x1, x2, x3 being object such that

A6: x1 in F

A7: x2 in F

A8: x3 in F

A9: i = [x1,x2,x3] by MCART_1:68;

M . (x1,x2) = F

then A10: [:F

.= {|M,M|} . (x1,x2,x3) by A6, A7, A8, ALTCAT_1:def 4

.= {|M,M|} . i by A9, MULTOP_1:def 1 ;

A11: {|M|} . i = {|M|} . (x1,x2,x3) by A9, MULTOP_1:def 1

.= M . (x1,x3) by A6, A7, A8, ALTCAT_1:def 3 ;

A12: now :: thesis: ( {|M,M|} . i <> {} implies {|M|} . i <> {} )

A16: c . i =
c . (x1,x2,x3)
by A9, MULTOP_1:def 1
assume
{|M,M|} . i <> {}
; :: thesis: {|M|} . i <> {}

then consider j being object such that

A13: j in [:F_{2}(x2,x3),F_{2}(x1,x2):]
by A10, XBOOLE_0:def 1;

consider j1, j2 being object such that

A14: j1 in F_{2}(x2,x3)
and

A15: j2 in F_{2}(x1,x2)
and

j = [j1,j2] by A13, ZFMISC_1:84;

reconsider j2 = j2 as Function by A15;

reconsider j1 = j1 as Function by A14;

j1 * j2 in F_{2}(x1,x3)
by A1, A6, A7, A8, A14, A15;

hence {|M|} . i <> {} by A2, A6, A8, A11; :: thesis: verum

end;then consider j being object such that

A13: j in [:F

consider j1, j2 being object such that

A14: j1 in F

A15: j2 in F

j = [j1,j2] by A13, ZFMISC_1:84;

reconsider j2 = j2 as Function by A15;

reconsider j1 = j1 as Function by A14;

j1 * j2 in F

hence {|M|} . i <> {} by A2, A6, A8, A11; :: thesis: verum

.= FuncComp (F

then reconsider ci = c . i as Function ;

A17: dom ci = [:F

rng (FuncComp (F

proof

then
rng ci c= {|M|} . i
by A2, A6, A8, A16, A11;
set F = FuncComp (F_{2}(x1,x2),F_{2}(x2,x3));

let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in rng (FuncComp (F_{2}(x1,x2),F_{2}(x2,x3))) or i in F_{2}(x1,x3) )

assume i in rng (FuncComp (F_{2}(x1,x2),F_{2}(x2,x3)))
; :: thesis: i in F_{2}(x1,x3)

then consider j being object such that

A18: j in dom (FuncComp (F_{2}(x1,x2),F_{2}(x2,x3)))
and

A19: i = (FuncComp (F_{2}(x1,x2),F_{2}(x2,x3))) . j
by FUNCT_1:def 3;

consider f, g being Function such that

A20: j = [g,f] and

A21: (FuncComp (F_{2}(x1,x2),F_{2}(x2,x3))) . j = g * f
by A18, ALTCAT_1:def 9;

( g in F_{2}(x2,x3) & f in F_{2}(x1,x2) )
by A18, A20, ZFMISC_1:87;

hence i in F_{2}(x1,x3)
by A1, A6, A7, A8, A19, A21; :: thesis: verum

end;let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in rng (FuncComp (F

assume i in rng (FuncComp (F

then consider j being object such that

A18: j in dom (FuncComp (F

A19: i = (FuncComp (F

consider f, g being Function such that

A20: j = [g,f] and

A21: (FuncComp (F

( g in F

hence i in F

hence c . i is Function of ({|M,M|} . i),({|M|} . i) by A17, A10, A12, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

set C = AltCatStr(# F

take AltCatStr(# F

( the Arrows of AltCatStr(# F

thus the carrier of AltCatStr(# F

( the Arrows of AltCatStr(# F

let i, j be Element of F

thus the Arrows of AltCatStr(# F

let i, j, k be Element of F

thus the Comp of AltCatStr(# F