let C1, C2 be Coherence_Space; :: thesis: for a being Element of C1 [*] C2 holds
( proj1 a in C1 & proj2 a in C2 & a c= [:(proj1 a),(proj2 a):] )
let a be Element of C1 [*] C2; :: thesis: ( proj1 a in C1 & proj2 a in C2 & a c= [:(proj1 a),(proj2 a):] )
consider a1 being Element of C1, a2 being Element of C2 such that
A1: a c= [:a1,a2:] by Th96;
( proj1 a c= a1 & proj2 a c= a2 ) by A1, FUNCT_5:11;
hence ( proj1 a in C1 & proj2 a in C2 ) by CLASSES1:def 1; :: thesis: a c= [:(proj1 a),(proj2 a):]
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a or x in [:(proj1 a),(proj2 a):] )
assume A2: x in a ; :: thesis: x in [:(proj1 a),(proj2 a):]
then A3: x = [(x `1),(x `2)] by A1, MCART_1:21;
then ( x `1 in proj1 a & x `2 in proj2 a ) by A2, XTUPLE_0:def 12, XTUPLE_0:def 13;
hence x in [:(proj1 a),(proj2 a):] by A3, ZFMISC_1:87; :: thesis: verum