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 Th97;
( proj1 a c= a1 & proj2 a c= a2 ) by A1, FUNCT_5:13;
hence ( proj1 a in C1 & proj2 a in C2 ) by CLASSES1:def 1; :: thesis: a c= [:(proj1 a),(proj2 a):]
let x be set ; :: 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:23;
then ( x `1 in proj1 a & x `2 in proj2 a ) by A2, FUNCT_5:4;
hence x in [:(proj1 a),(proj2 a):] by A3, ZFMISC_1:106; :: thesis: verum