set A = F1();
defpred S1[ set , set ] means ex a, b being set st
( $1 = [a,b] & ( for f being set holds
( f in $2 iff ( f in Funcs (F2(a),F2(b)) & P1[a,b,f] ) ) ) );
A3:
now let x be
set ;
( x in [:F1(),F1():] implies ex y being set st S1[x,y] )assume
x in [:F1(),F1():]
;
ex y being set st S1[x,y]then consider a,
b being
set such that
a in F1()
and
b in F1()
and A4:
x = [a,b]
by ZFMISC_1:def 2;
defpred S2[
set ]
means P1[
a,
b,$1];
consider y being
set such that A5:
for
f being
set holds
(
f in y iff (
f in Funcs (
F2(
a),
F2(
b)) &
S2[
f] ) )
from XBOOLE_0:sch 1();
take y =
y;
S1[x,y]thus
S1[
x,
y]
by A4, A5;
verum end;
consider F being Function such that
dom F = [:F1(),F1():]
and
A6:
for x being set st x in [:F1(),F1():] holds
S1[x,F . x]
from CLASSES1:sch 1(A3);
A7:
now let a,
b be
set ;
( a in F1() & b in F1() implies for f being set holds
( f in F . [a,b] iff ( P1[a,b,f] & f in Funcs (F2(a),F2(b)) ) ) )assume that A8:
a in F1()
and A9:
b in F1()
;
for f being set holds
( f in F . [a,b] iff ( P1[a,b,f] & f in Funcs (F2(a),F2(b)) ) )
[a,b] in [:F1(),F1():]
by A8, A9, ZFMISC_1:87;
then consider a9,
b9 being
set such that A10:
[a,b] = [a9,b9]
and A11:
for
f being
set holds
(
f in F . [a,b] iff (
f in Funcs (
F2(
a9),
F2(
b9)) &
P1[
a9,
b9,
f] ) )
by A6;
A12:
a = a9
by A10, ZFMISC_1:27;
A13:
b = b9
by A10, ZFMISC_1:27;
let f be
set ;
( f in F . [a,b] iff ( P1[a,b,f] & f in Funcs (F2(a),F2(b)) ) )thus
(
f in F . [a,b] iff (
P1[
a,
b,
f] &
f in Funcs (
F2(
a),
F2(
b)) ) )
by A11, A12, A13;
verum end;
deffunc H1( set , set ) -> set = F . [$1,$2];
A14:
now let a,
b,
c be
Element of
F1();
for f, g being Function st f in H1(a,b) & g in H1(b,c) holds
g * f in H1(a,c)let f,
g be
Function;
( f in H1(a,b) & g in H1(b,c) implies g * f in H1(a,c) )assume that A15:
f in H1(
a,
b)
and A16:
g in H1(
b,
c)
;
g * f in H1(a,c)A17:
P1[
a,
b,
f]
by A7, A15;
A18:
f in Funcs (
F2(
a),
F2(
b))
by A7, A15;
A19:
P1[
b,
c,
g]
by A7, A16;
A20:
g in Funcs (
F2(
b),
F2(
c))
by A7, A16;
A21:
dom f = F2(
a)
by A18, Th31;
A22:
rng f c= F2(
b)
by A18, Th31;
A23:
dom g = F2(
b)
by A20, Th31;
A24:
rng g c= F2(
c)
by A20, Th31;
A25:
rng (g * f) c= rng g
by RELAT_1:26;
A26:
dom (g * f) = F2(
a)
by A21, A22, A23, RELAT_1:27;
rng (g * f) c= F2(
c)
by A24, A25, XBOOLE_1:1;
then A27:
g * f in Funcs (
F2(
a),
F2(
c))
by A26, FUNCT_2:def 2;
P1[
a,
c,
g * f]
by A1, A17, A19;
hence
g * f in H1(
a,
c)
by A7, A27;
verum end;
A29:
for a being Element of F1() holds id F2(a) in H1(a,a)
consider C being strict semi-functional para-functional set-id-inheriting category such that
A33:
the carrier of C = F1()
and
A34:
for a being object of C holds the_carrier_of a = F2(a)
and
A35:
for a, b being object of C holds <^a,b^> = H1(a,b)
from YELLOW18:sch 16(A14, A28, A29);
take
C
; ( the carrier of C = F1() & ( for a being object of C holds the_carrier_of a = F2(a) ) & ( for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C . (a,b) iff ( f in Funcs (F2(a),F2(b)) & P1[a,b,f] ) ) ) )
thus
the carrier of C = F1()
by A33; ( ( for a being object of C holds the_carrier_of a = F2(a) ) & ( for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C . (a,b) iff ( f in Funcs (F2(a),F2(b)) & P1[a,b,f] ) ) ) )
thus
for a being object of C holds the_carrier_of a = F2(a)
by A34; for a, b being Element of F1()
for f being Function holds
( f in the Arrows of C . (a,b) iff ( f in Funcs (F2(a),F2(b)) & P1[a,b,f] ) )
let a, b be Element of F1(); for f being Function holds
( f in the Arrows of C . (a,b) iff ( f in Funcs (F2(a),F2(b)) & P1[a,b,f] ) )
let f be Function; ( f in the Arrows of C . (a,b) iff ( f in Funcs (F2(a),F2(b)) & P1[a,b,f] ) )
reconsider a = a, b = b as object of C by A33;
the Arrows of C . (a,b) =
<^a,b^>
.=
F . [a,b]
by A35
;
hence
( f in the Arrows of C . (a,b) iff ( f in Funcs (F2(a),F2(b)) & P1[a,b,f] ) )
by A7; verum