consider M being ManySortedSet of such that
A2:
for i, j being Element of F1() holds M . i,j = F2(i,j)
from ALTCAT_1:sch 2();
deffunc H1( set , set , set ) -> set = FuncComp F2($1,$2),F2($2,$3);
consider c being ManySortedSet of such that
A3:
for i, j, k being Element of F1() holds c . i,j,k = H1(i,j,k)
from ALTCAT_1:sch 4();
c is Function-yielding
proof
let i be
set ;
:: 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():]
by PARTFUN1:def 4;
then consider x1,
x2,
x3 being
set such that A4:
(
x1 in F1() &
x2 in F1() &
x3 in F1() )
and A5:
i = [x1,x2,x3]
by MCART_1:72;
c . i =
c . x1,
x2,
x3
by A5, MULTOP_1:def 1
.=
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 ;
now let i be
set ;
:: 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
set such that A6:
(
x1 in F1() &
x2 in F1() &
x3 in F1() )
and A7:
i = [x1,x2,x3]
by MCART_1:72;
A8:
M . x1,
x2 = F2(
x1,
x2)
by A2, A6;
A9:
c . i =
c . x1,
x2,
x3
by A7, MULTOP_1:def 1
.=
FuncComp F2(
x1,
x2),
F2(
x2,
x3)
by A3, A6
;
then reconsider ci =
c . i as
Function ;
A10:
dom ci = [:F2(x2,x3),F2(x1,x2):]
by A9, PARTFUN1:def 4;
A11:
[:F2(x2,x3),F2(x1,x2):] =
[:(M . x2,x3),(M . x1,x2):]
by A2, A6, A8
.=
{|M,M|} . x1,
x2,
x3
by A6, ALTCAT_1:def 6
.=
{|M,M|} . i
by A7, MULTOP_1:def 1
;
A12:
rng (FuncComp F2(x1,x2),F2(x2,x3)) c= F2(
x1,
x3)
proof
let i be
set ;
:: according to TARSKI:def 3 :: thesis: ( not i in rng (FuncComp F2(x1,x2),F2(x2,x3)) or i in F2(x1,x3) )
set F =
FuncComp F2(
x1,
x2),
F2(
x2,
x3);
assume
i in rng (FuncComp F2(x1,x2),F2(x2,x3))
;
:: thesis: i in F2(x1,x3)
then consider j being
set such that A13:
j in dom (FuncComp F2(x1,x2),F2(x2,x3))
and A14:
i = (FuncComp F2(x1,x2),F2(x2,x3)) . j
by FUNCT_1:def 5;
consider f,
g being
Function such that A15:
j = [g,f]
and A16:
(FuncComp F2(x1,x2),F2(x2,x3)) . j = g * f
by A13, ALTCAT_1:def 11;
dom (FuncComp F2(x1,x2),F2(x2,x3)) = [:F2(x2,x3),F2(x1,x2):]
by PARTFUN1:def 4;
then
(
g in F2(
x2,
x3) &
f in F2(
x1,
x2) )
by A13, A15, ZFMISC_1:106;
hence
i in F2(
x1,
x3)
by A1, A6, A14, A16;
:: thesis: verum
end; A17:
{|M|} . i =
{|M|} . x1,
x2,
x3
by A7, MULTOP_1:def 1
.=
M . x1,
x3
by A6, ALTCAT_1:def 5
;
then A18:
rng ci c= {|M|} . i
by A2, A6, A9, A12;
now assume
{|M,M|} . i <> {}
;
:: thesis: {|M|} . i <> {} then consider j being
set such that A19:
j in [:F2(x2,x3),F2(x1,x2):]
by A11, XBOOLE_0:def 1;
consider j1,
j2 being
set such that A20:
j1 in F2(
x2,
x3)
and A21:
j2 in F2(
x1,
x2)
and
j = [j1,j2]
by A19, ZFMISC_1:103;
reconsider j1 =
j1 as
Function by A20;
reconsider j2 =
j2 as
Function by A21;
j1 * j2 in F2(
x1,
x3)
by A1, A6, A20, A21;
hence
{|M|} . i <> {}
by A2, A6, A17;
:: thesis: verum end; hence
c . i is
Function of
({|M,M|} . i),
({|M|} . i)
by A10, A11, A18, FUNCT_2:def 1, RELSET_1:11;
:: thesis: verum end;
then reconsider c = c as BinComp of M by PBOOLE:def 18;
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