deffunc H1( set , set , set ) -> set = FuncComp (F2(\$1,\$2),F2(\$2,\$3));
consider M being ManySortedSet of [:F1(),F1():] such that
A2: for i, j being Element of F1() holds M . (i,j) = F2(i,j) from consider c being ManySortedSet of [:F1(),F1(),F1():] such that
A3: for i, j, k being Element of F1() holds c . (i,j,k) = H1(i,j,k) from c is Function-yielding
proof
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 [:F1(),F1(),F1():] ;
then consider x1, x2, x3 being object such that
A4: ( x1 in F1() & x2 in F1() & x3 in F1() ) and
A5: i = [x1,x2,x3] by MCART_1:68;
c . i = c . (x1,x2,x3) by
.= FuncComp (F2(x1,x2),F2(x2,x3)) by A3, A4 ;
hence c . i is set ; :: thesis: verum
end;
then reconsider c = c as ManySortedFunction of [:F1(),F1(),F1():] ;
now :: thesis: for i being object st i in [:F1(),F1(),F1():] holds
c . i is Function of ({|M,M|} . i),({|M|} . i)
let i be object ; :: thesis: ( i in [:F1(),F1(),F1():] implies c . i is Function of ({|M,M|} . i),({|M|} . i) )
assume i in [:F1(),F1(),F1():] ; :: thesis: c . i is Function of ({|M,M|} . i),({|M|} . i)
then consider x1, x2, x3 being object such that
A6: x1 in F1() and
A7: x2 in F1() and
A8: x3 in F1() and
A9: i = [x1,x2,x3] by MCART_1:68;
M . (x1,x2) = F2(x1,x2) by A2, A6, A7;
then A10: [:F2(x2,x3),F2(x1,x2):] = [:(M . (x2,x3)),(M . (x1,x2)):] by A2, A7, A8
.= {|M,M|} . (x1,x2,x3) by
.= {|M,M|} . i by ;
A11: {|M|} . i = {|M|} . (x1,x2,x3) by
.= M . (x1,x3) by ;
A12: now :: thesis: ( {|M,M|} . i <> {} implies {|M|} . i <> {} )
assume {|M,M|} . i <> {} ; :: thesis:
then consider j being object such that
A13: j in [:F2(x2,x3),F2(x1,x2):] by ;
consider j1, j2 being object such that
A14: j1 in F2(x2,x3) and
A15: j2 in F2(x1,x2) and
j = [j1,j2] by ;
reconsider j2 = j2 as Function by A15;
reconsider j1 = j1 as Function by A14;
j1 * j2 in F2(x1,x3) by A1, A6, A7, A8, A14, A15;
hence {|M|} . i <> {} by A2, A6, A8, A11; :: thesis: verum
end;
A16: c . i = c . (x1,x2,x3) by
.= FuncComp (F2(x1,x2),F2(x2,x3)) by A3, A6, A7, A8 ;
then reconsider ci = c . i as Function ;
A17: dom ci = [:F2(x2,x3),F2(x1,x2):] by ;
rng (FuncComp (F2(x1,x2),F2(x2,x3))) c= F2(x1,x3)
proof
set F = FuncComp (F2(x1,x2),F2(x2,x3));
let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in rng (FuncComp (F2(x1,x2),F2(x2,x3))) or i in F2(x1,x3) )
assume i in rng (FuncComp (F2(x1,x2),F2(x2,x3))) ; :: thesis: i in F2(x1,x3)
then consider j being object such that
A18: j in dom (FuncComp (F2(x1,x2),F2(x2,x3))) and
A19: i = (FuncComp (F2(x1,x2),F2(x2,x3))) . j by FUNCT_1:def 3;
consider f, g being Function such that
A20: j = [g,f] and
A21: (FuncComp (F2(x1,x2),F2(x2,x3))) . j = g * f by ;
( g in F2(x2,x3) & f in F2(x1,x2) ) by ;
hence i in F2(x1,x3) by A1, A6, A7, A8, A19, A21; :: thesis: verum
end;
then rng ci c= {|M|} . i by A2, A6, A8, A16, A11;
hence c . i is Function of ({|M,M|} . i),({|M|} . i) by ; :: thesis: verum
end;
then reconsider c = c as BinComp of M by PBOOLE:def 15;
set C = AltCatStr(# F1(),M,c #);
take AltCatStr(# F1(),M,c #) ; :: thesis: ( the carrier of AltCatStr(# F1(),M,c #) = F1() & ( for i, j being Element of F1() holds
( the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) ) ) )

thus the carrier of AltCatStr(# F1(),M,c #) = F1() ; :: thesis: for i, j being Element of F1() holds
( the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) )

let i, j be Element of F1(); :: thesis: ( the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) & ( for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) ) )
thus the Arrows of AltCatStr(# F1(),M,c #) . (i,j) = F2(i,j) by A2; :: thesis: for i, j, k being Element of F1() holds the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k))
let i, j, k be Element of F1(); :: thesis: the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k))
thus the Comp of AltCatStr(# F1(),M,c #) . (i,j,k) = FuncComp (F2(i,j),F2(j,k)) by A3; :: thesis: verum