deffunc H1( set ) -> set = F2(($1 `1 ),($1 `2 ));
defpred S1[ set , set ] means P1[$1 `1 ,$1 `2 ,$2];
deffunc H2( set , set , set , set , set ) -> set = F3($1,$2,$3,$4,$5);
consider P being Function such that
dom P = [:F1(),F1():] and
A5: for i being set st i in [:F1(),F1():] holds
for x being set holds
( x in P . i iff ( x in H1(i) & S1[i,x] ) ) from CARD_3:sch 4();
 deffunc H3( set , set ) -> set = P . $1,$2;
A6: now
let a, b be Element of F1(); :: thesis: for x being set holds
( x in P . a,b iff ( x in F2(a,b) & P1[a,b,x] ) )
let x be set ; :: thesis: ( x in P . a,b iff ( x in F2(a,b) & P1[a,b,x] ) )
A7: [a,b] `1 = a by MCART_1:7;
A8: [a,b] `2 = b by MCART_1:7;
[a,b] in [:F1(),F1():] by ZFMISC_1:def 2;
hence ( x in P . a,b iff ( x in F2(a,b) & P1[a,b,x] ) ) by A5, A7, A8; :: thesis: verum
end;
A9: now
let a, b, c be Element of F1(); :: thesis: for f, g being set st f in H3(a,b) & g in H3(b,c) holds
H2(a,b,c,f,g) in H3(a,c)
let f, g be set ; :: thesis: ( f in H3(a,b) & g in H3(b,c) implies H2(a,b,c,f,g) in H3(a,c) )
assume that
A10: f in H3(a,b) and
A11: g in H3(b,c) ; :: thesis: H2(a,b,c,f,g) in H3(a,c)
A12: f in F2(a,b) by A6, A10;
A13: P1[a,b,f] by A6, A10;
A14: g in F2(b,c) by A6, A11;
A15: P1[b,c,g] by A6, A11;
then A16: H2(a,b,c,f,g) in F2(a,c) by A1, A12, A13, A14;
P1[a,c,H2(a,b,c,f,g)] by A1, A12, A13, A14, A15;
hence H2(a,b,c,f,g) in H3(a,c) by A6, A16; :: thesis: verum
end;
A17: now
let a, b, c, d be Element of F1(); :: thesis: for f, g, h being set st f in H3(a,b) & g in H3(b,c) & h in H3(c,d) holds
H2(a,c,d,H2(a,b,c,f,g),h) = H2(a,b,d,f,H2(b,c,d,g,h))
let f, g, h be set ; :: thesis: ( f in H3(a,b) & g in H3(b,c) & h in H3(c,d) implies H2(a,c,d,H2(a,b,c,f,g),h) = H2(a,b,d,f,H2(b,c,d,g,h)) )
assume that
A18: f in H3(a,b) and
A19: g in H3(b,c) and
A20: h in H3(c,d) ; :: thesis: H2(a,c,d,H2(a,b,c,f,g),h) = H2(a,b,d,f,H2(b,c,d,g,h))
A21: f in F2(a,b) by A6, A18;
A22: P1[a,b,f] by A6, A18;
A23: g in F2(b,c) by A6, A19;
A24: P1[b,c,g] by A6, A19;
A25: h in F2(c,d) by A6, A20;
P1[c,d,h] by A6, A20;
hence H2(a,c,d,H2(a,b,c,f,g),h) = H2(a,b,d,f,H2(b,c,d,g,h)) by A2, A21, A22, A23, A24, A25; :: thesis: verum
end;
A26: now
let a be Element of F1(); :: thesis: ex f being set st
( f in H3(a,a) & ( for b being Element of F1()
for g being set st g in H3(a,b) holds
H2(a,a,b,f,g) = g ) )
consider f being set such that
A27: f in F2(a,a) and
A28: P1[a,a,f] and
A29: for b being Element of F1()
for g being set st g in F2(a,b) & P1[a,b,g] holds
H2(a,a,b,f,g) = g by A3;
take f = f; :: thesis: ( f in H3(a,a) & ( for b being Element of F1()
for g being set st g in H3(a,b) holds
H2(a,a,b,f,g) = g ) )
thus f in H3(a,a) by A6, A27, A28; :: thesis: for b being Element of F1()
for g being set st g in H3(a,b) holds
H2(a,a,b,f,g) = g
let b be Element of F1(); :: thesis: for g being set st g in H3(a,b) holds
H2(a,a,b,f,g) = g
let g be set ; :: thesis: ( g in H3(a,b) implies H2(a,a,b,f,g) = g )
assume A30: g in H3(a,b) ; :: thesis: H2(a,a,b,f,g) = g
then A31: g in F2(a,b) by A6;
P1[a,b,g] by A6, A30;
hence H2(a,a,b,f,g) = g by A29, A31; :: thesis: verum
end;
A32: now
let a be Element of F1(); :: thesis: ex f being set st
( f in H3(a,a) & ( for b being Element of F1()
for g being set st g in H3(b,a) holds
H2(b,a,a,g,f) = g ) )
consider f being set such that
A33: f in F2(a,a) and
A34: P1[a,a,f] and
A35: for b being Element of F1()
for g being set st g in F2(b,a) & P1[b,a,g] holds
H2(b,a,a,g,f) = g by A4;
take f = f; :: thesis: ( f in H3(a,a) & ( for b being Element of F1()
for g being set st g in H3(b,a) holds
H2(b,a,a,g,f) = g ) )
thus f in H3(a,a) by A6, A33, A34; :: thesis: for b being Element of F1()
for g being set st g in H3(b,a) holds
H2(b,a,a,g,f) = g
let b be Element of F1(); :: thesis: for g being set st g in H3(b,a) holds
H2(b,a,a,g,f) = g
let g be set ; :: thesis: ( g in H3(b,a) implies H2(b,a,a,g,f) = g )
assume A36: g in H3(b,a) ; :: thesis: H2(b,a,a,g,f) = g
then A37: g in F2(b,a) by A6;
P1[b,a,g] by A6, A36;
hence H2(b,a,a,g,f) = g by A35, A37; :: thesis: verum
end;
consider C being strict category such that
A38: the carrier of C = F1() and
A39: for a, b being object of C holds <^a,b^> = H3(a,b) and
A40: for a, b, c being object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = H2(a,b,c,f,g) from YELLOW18:sch 4(A9, A17, A26, A32);
 take C ; :: thesis: ( the carrier of C = F1() & ( for a, b being object of C
for f being set holds
( f in <^a,b^> iff ( f in F2(a,b) & P1[a,b,f] ) ) ) & ( for a, b, c being object of C 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 C = F1() by A38; :: thesis: ( ( for a, b being object of C
for f being set holds
( f in <^a,b^> iff ( f in F2(a,b) & P1[a,b,f] ) ) ) & ( for a, b, c being object of C 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) ) )
hereby :: thesis: for a, b, c being object of C 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 be object of C; :: thesis: for f being set holds
( f in <^a,b^> iff ( f in F2(a,b) & P1[a,b,f] ) )
let f be set ; :: thesis: ( f in <^a,b^> iff ( f in F2(a,b) & P1[a,b,f] ) )
<^a,b^> = P . a,b by A39;
hence ( f in <^a,b^> iff ( f in F2(a,b) & P1[a,b,f] ) ) by A6, A38; :: thesis: verum
end;
thus for a, b, c being object of C 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) by A40; :: thesis: verum