let A, B be AltCatStr ; ( A,B have_the_same_composition implies for a1, a2 being Object of A
for b1, b2 being Object of B
for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> )
assume A1:
A,B have_the_same_composition
; for a1, a2 being Object of A
for b1, b2 being Object of B
for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
the carrier of (Intersect (A,B)) = the carrier of A /\ the carrier of B
by A1, Def3;
then A2:
[: the carrier of (Intersect (A,B)), the carrier of (Intersect (A,B)):] = [: the carrier of A, the carrier of A:] /\ [: the carrier of B, the carrier of B:]
by ZFMISC_1:100;
let a1, a2 be Object of A; for b1, b2 being Object of B
for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
let b1, b2 be Object of B; for o1, o2 being Object of (Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
let o1, o2 be Object of (Intersect (A,B)); ( o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 implies <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> )
assume A3:
( o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 )
; <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
A4:
now ( the carrier of A <> {} & the carrier of B <> {} implies [o1,o2] in [: the carrier of (Intersect (A,B)), the carrier of (Intersect (A,B)):] )assume
( the
carrier of
A <> {} & the
carrier of
B <> {} )
;
[o1,o2] in [: the carrier of (Intersect (A,B)), the carrier of (Intersect (A,B)):]then
(
[a1,a2] in [: the carrier of A, the carrier of A:] &
[b1,b2] in [: the carrier of B, the carrier of B:] )
by ZFMISC_1:def 2;
hence
[o1,o2] in [: the carrier of (Intersect (A,B)), the carrier of (Intersect (A,B)):]
by A3, A2, XBOOLE_0:def 4;
verum end;
A5:
( dom the Arrows of A = [: the carrier of A, the carrier of A:] & dom the Arrows of B = [: the carrier of B, the carrier of B:] )
by PARTFUN1:def 2;
A6:
now ( ( the carrier of A = {} or the carrier of B = {} ) implies ( ( the Arrows of A . [a1,a2]) /\ ( the Arrows of B . [b1,b2]) = {} & the Arrows of (Intersect (A,B)) . [o1,o2] = {} ) )assume
( the
carrier of
A = {} or the
carrier of
B = {} )
;
( ( the Arrows of A . [a1,a2]) /\ ( the Arrows of B . [b1,b2]) = {} & the Arrows of (Intersect (A,B)) . [o1,o2] = {} )then A7:
(
[: the carrier of A, the carrier of A:] = {} or
[: the carrier of B, the carrier of B:] = {} )
by ZFMISC_1:90;
then
( the
Arrows of
A . [a1,a2] = {} or the
Arrows of
B . [b1,b2] = {} )
;
hence
(
( the Arrows of A . [a1,a2]) /\ ( the Arrows of B . [b1,b2]) = {} & the
Arrows of
(Intersect (A,B)) . [o1,o2] = {} )
by A2, A7;
verum end;
the Arrows of (Intersect (A,B)) = Intersect ( the Arrows of A, the Arrows of B)
by A1, Def3;
hence
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
by A3, A2, A5, A4, A6, Def2; verum