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 ;
( i in [:F1(),F1(),F1():] implies ex j being object st S1[i,j] )
assume
i in [:F1(),F1(),F1():]
;
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 ;
( 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):]
;
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);
( y in F2(a,c) & S2[x,y] )
thus
y in F2(
a,
c)
by A1, A9, A10;
S2[x,y]
thus
S2[
x,
y]
by A11;
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;
S1[i,j]
take
a
;
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
;
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
;
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
;
( 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;
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 ;
( 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)
;
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;
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 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 ;
( i in [:F1(),F1(),F1():] implies C . i is Function of ({|B,B|} . i),({|B|} . i) )assume
i in [:F1(),F1(),F1():]
;
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;
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 #);
ALTCAT_1:def 2 ( <^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^> <> {}
;
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;
verum
end;
then reconsider alt = AltCatStr(# F1(),B,C #) as non empty transitive strict AltCatStr ;
take
alt
; ( 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()
; ( ( 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; 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; ( <^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^> <> {}
; 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; for g being Morphism of b,c holds g * f = F3(a,b,c,f,g)
let g be Morphism of b,c; 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
; verum