consider B being ManySortedSet of [:F1(),F1():] such that
A2: for a, b being Element of F1() holds B . (a,b) = F2(a,b) from ALTCAT_1:sch 2();
 defpred S1[ object , object ] means ex a, b, c being Element of F1() ex F being Function of ({|B,B|} . (a,b,c)),({|B|} . (a,b,c)) st
( $1 = [a,b,c] & $2 = F & ( for f, g being object st f in F2(a,b) & g in F2(b,c) holds
F . [g,f] = F3(a,b,c,f,g) ) );
A3: for i being object st i in [:F1(),F1(),F1():] holds
ex j being object st S1[i,j]
proof
let i be object ; :: thesis: ( i in [:F1(),F1(),F1():] implies ex j being object st S1[i,j] )
assume i in [:F1(),F1(),F1():] ; :: thesis: ex j being object st S1[i,j]
then consider a, b, c being object such that
A4: a in F1() and
A5: b in F1() and
A6: c in F1() and
A7: i = [a,b,c] by MCART_1:68;
reconsider a = a, b = b, c = c as Element of F1() by A4, A5, A6;
defpred S2[ object , object ] means ex f, g being object st
( $1 = [g,f] & $2 = F3(a,b,c,f,g) );
A8: for x being object st x in [:F2(b,c),F2(a,b):] holds
ex y being object st
( y in F2(a,c) & S2[x,y] )
proof
let x be object ; :: thesis: ( x in [:F2(b,c),F2(a,b):] implies ex y being object st
( y in F2(a,c) & S2[x,y] ) )
assume x in [:F2(b,c),F2(a,b):] ; :: thesis: ex y being object st
( y in F2(a,c) & S2[x,y] )
then consider x1, x2 being object such that
A9: x1 in F2(b,c) and
A10: x2 in F2(a,b) and
A11: x = [x1,x2] by ZFMISC_1:def 2;
take y = F3(a,b,c,x2,x1); :: thesis: ( y in F2(a,c) & S2[x,y] )
thus y in F2(a,c) by A1, A9, A10; :: thesis: S2[x,y]
thus S2[x,y] by A11; :: thesis: verum
end;
consider F being Function such that
A12: ( dom F = [:F2(b,c),F2(a,b):] & rng F c= F2(a,c) ) and
A13: for x being object st x in [:F2(b,c),F2(a,b):] holds
S2[x,F . x] from FUNCT_1:sch 6(A8);
 A14: B . (a,b) = F2(a,b) by A2;
A15: B . (b,c) = F2(b,c) by A2;
A16: B . (a,c) = F2(a,c) by A2;
A17: {|B,B|} . (a,b,c) = [:F2(b,c),F2(a,b):] by A14, A15, ALTCAT_1:def 4;
{|B|} . (a,b,c) = F2(a,c) by A16, ALTCAT_1:def 3;
then reconsider F = F as Function of ({|B,B|} . (a,b,c)),({|B|} . (a,b,c)) by A12, A17, FUNCT_2:2;
take j = F; :: thesis: S1[i,j]
take a ; :: thesis: ex b, c being Element of F1() ex F being Function of ({|B,B|} . (a,b,c)),({|B|} . (a,b,c)) st
( i = [a,b,c] & j = F & ( for f, g being object st f in F2(a,b) & g in F2(b,c) holds
F . [g,f] = F3(a,b,c,f,g) ) )
take b ; :: thesis: ex c being Element of F1() ex F being Function of ({|B,B|} . (a,b,c)),({|B|} . (a,b,c)) st
( i = [a,b,c] & j = F & ( for f, g being object st f in F2(a,b) & g in F2(b,c) holds
F . [g,f] = F3(a,b,c,f,g) ) )
take c ; :: thesis: ex F being Function of ({|B,B|} . (a,b,c)),({|B|} . (a,b,c)) st
( i = [a,b,c] & j = F & ( for f, g being object st f in F2(a,b) & g in F2(b,c) holds
F . [g,f] = F3(a,b,c,f,g) ) )
take F ; :: thesis: ( i = [a,b,c] & j = F & ( for f, g being object st f in F2(a,b) & g in F2(b,c) holds
F . [g,f] = F3(a,b,c,f,g) ) )
thus ( i = [a,b,c] & j = F ) by A7; :: thesis: for f, g being object st f in F2(a,b) & g in F2(b,c) holds
F . [g,f] = F3(a,b,c,f,g)
let f, g be object ; :: thesis: ( f in F2(a,b) & g in F2(b,c) implies F . [g,f] = F3(a,b,c,f,g) )
assume that
A18: f in F2(a,b) and
A19: g in F2(b,c) ; :: thesis: F . [g,f] = F3(a,b,c,f,g)
[g,f] in [:F2(b,c),F2(a,b):] by A18, A19, ZFMISC_1:87;
then consider f9, g9 being object such that
A20: [g,f] = [g9,f9] and
A21: F . [g,f] = F3(a,b,c,f9,g9) by A13;
g = g9 by A20, XTUPLE_0:1;
hence F . [g,f] = F3(a,b,c,f,g) by A20, A21, XTUPLE_0:1; :: thesis: verum
end;
consider C being Function such that
A22: dom C = [:F1(),F1(),F1():] and
A23: for i being object st i in [:F1(),F1(),F1():] holds
S1[i,C . i] from CLASSES1:sch 1(A3);
 reconsider C = C as ManySortedSet of [:F1(),F1(),F1():] by A22, PARTFUN1:def 2, RELAT_1:def 18;
now :: thesis: for i being object st i in [:F1(),F1(),F1():] holds
C . i is Function of ({|B,B|} . i),({|B|} . i)
let i be object ; :: thesis: ( i in [:F1(),F1(),F1():] implies C . i is Function of ({|B,B|} . i),({|B|} . i) )
assume i in [:F1(),F1(),F1():] ; :: thesis: C . i is Function of ({|B,B|} . i),({|B|} . i)
then consider a, b, c being Element of F1(), F being Function of ({|B,B|} . (a,b,c)),({|B|} . (a,b,c)) such that
A24: i = [a,b,c] and
A25: C . i = F and
for f, g being object st f in F2(a,b) & g in F2(b,c) holds
F . [g,f] = F3(a,b,c,f,g) by A23;
A26: {|B|} . (a,b,c) = {|B|} . i by A24, MULTOP_1:def 1;
{|B,B|} . (a,b,c) = {|B,B|} . i by A24, MULTOP_1:def 1;
hence C . i is Function of ({|B,B|} . i),({|B|} . i) by A25, A26; :: thesis: verum
end;
then reconsider C = C as ManySortedFunction of {|B,B|},{|B|} by PBOOLE:def 15;
set alt = AltCatStr(# F1(),B,C #);
AltCatStr(# F1(),B,C #) is transitive
proof
let o1, o2, o3 be Object of AltCatStr(# F1(),B,C #); :: according to ALTCAT_1:def 2 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
reconsider a = o1, b = o2, c = o3 as Element of F1() ;
set f = the Element of <^o1,o2^>;
set g = the Element of <^o2,o3^>;
assume that
A27: <^o1,o2^> <> {} and
A28: <^o2,o3^> <> {} ; :: thesis: not <^o1,o3^> = {}
A29: the Element of <^o1,o2^> in <^o1,o2^> by A27;
A30: the Element of <^o2,o3^> in <^o2,o3^> by A28;
A31: the Element of <^o1,o2^> in F2(a,b) by A2, A29;
the Element of <^o2,o3^> in F2(b,c) by A2, A30;
then F3(a,b,c, the Element of <^o1,o2^>, the Element of <^o2,o3^>) in F2(a,c) by A1, A31;
hence not <^o1,o3^> = {} by A2; :: thesis: verum
end;
then reconsider alt = AltCatStr(# F1(),B,C #) as non empty transitive strict AltCatStr ;
take alt ; :: thesis: ( the carrier of alt = F1() & ( for a, b being Object of alt holds <^a,b^> = F2(a,b) ) & ( for a, b, c being Object of alt st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) )
thus the carrier of alt = F1() ; :: thesis: ( ( for a, b being Object of alt holds <^a,b^> = F2(a,b) ) & ( for a, b, c being Object of alt st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) ) )
thus for a, b being Object of alt holds <^a,b^> = F2(a,b) by A2; :: thesis: for a, b, c being Object of alt st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g)
let a, b, c be Object of alt; :: thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g) )
assume that
A32: <^a,b^> <> {} and
A33: <^b,c^> <> {} ; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F3(a,b,c,f,g)
[a,b,c] in [:F1(),F1(),F1():] by MCART_1:69;
then consider a9, b9, c9 being Element of F1(), F being Function of ({|B,B|} . (a9,b9,c9)),({|B|} . (a9,b9,c9)) such that
A34: [a,b,c] = [a9,b9,c9] and
A35: C . [a,b,c] = F and
A36: for f, g being object st f in F2(a9,b9) & g in F2(b9,c9) holds
F . [g,f] = F3(a9,b9,c9,f,g) by A23;
A37: a = a9 by A34, XTUPLE_0:3;
A38: b = b9 by A34, XTUPLE_0:3;
A39: c = c9 by A34, XTUPLE_0:3;
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c holds g * f = F3(a,b,c,f,g)
let g be Morphism of b,c; :: thesis: g * f = F3(a,b,c,f,g)
A40: <^a,b^> = F2(a,b) by A2;
<^b,c^> = F2(b,c) by A2;
then A41: F . [g,f] = F3(a,b,c,f,g) by A32, A33, A36, A37, A38, A39, A40;
thus g * f = ( the Comp of alt . (a,b,c)) . (g,f) by A32, A33, ALTCAT_1:def 8
.= F3(a,b,c,f,g) by A35, A41, MULTOP_1:def 1 ; :: thesis: verum