let R1, R2 be Relation; :: thesis: field (R1 \, R2) = (field R1) \/ (field R2)
thus field (R1 \, R2) c= (field R1) \/ (field R2) :: according to XBOOLE_0:def 10 :: thesis: (field R1) \/ (field R2) c= field (R1 \, R2)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in field (R1 \, R2) or z in (field R1) \/ (field R2) )
assume z in field (R1 \, R2) ; :: thesis: z in (field R1) \/ (field R2)
then ( z in dom (R1 \, R2) or z in rng (R1 \, R2) ) by XBOOLE_0:def 3;
then consider y being object such that
A1: ( [z,y] in R1 \, R2 or [y,z] in R1 \, R2 ) by XTUPLE_0:def 12, XTUPLE_0:def 13;
reconsider zz = z, y = y as set by TARSKI:1;
( zz,y in R1 \, R2 or y,zz in R1 \, R2 ) by A1;
then ( zz,y in R1 or y,zz in R1 or zz,y in R2 or y,zz in R2 ) by Th9;
then ( [z,y] in R1 or [y,z] in R1 or [z,y] in R2 or [y,z] in R2 ) ;
then ( z in field R1 or z in field R2 ) by RELAT_1:15;
hence z in (field R1) \/ (field R2) by XBOOLE_0:def 3; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (field R1) \/ (field R2) or z in field (R1 \, R2) )
assume z in (field R1) \/ (field R2) ; :: thesis: z in field (R1 \, R2)
then ( z in field R1 or z in field R2 ) by XBOOLE_0:def 3;
then ( z in dom R1 or z in rng R1 or z in dom R2 or z in rng R2 ) by XBOOLE_0:def 3;
then consider y being object such that
A2: ( [z,y] in R1 or [y,z] in R1 or [z,y] in R2 or [y,z] in R2 ) by XTUPLE_0:def 12, XTUPLE_0:def 13;
reconsider zz = z, y = y as set by TARSKI:1;
( zz,y in R1 or y,zz in R1 or ( zz,y in R2 & y,zz nin R1 ) or y,zz in R1 or ( y,zz in R2 & zz,y nin R1 ) or zz,y in R1 ) by A2;
then ( zz,y in R1 \, R2 or y,zz in R1 \, R2 ) by Th9;
then ( [z,y] in R1 \, R2 or [y,z] in R1 \, R2 ) ;
hence z in field (R1 \, R2) by RELAT_1:15; :: thesis: verum