let P, R be Relation; :: thesis: field (P \/ R) = (field P) \/ (field R)
thus field (P \/ R) = ((dom P) \/ (dom R)) \/ (rng (P \/ R)) by XTUPLE_0:23
.= ((dom P) \/ (dom R)) \/ ((rng P) \/ (rng R)) by XTUPLE_0:27
.= (((dom P) \/ (dom R)) \/ (rng P)) \/ (rng R) by XBOOLE_1:4
.= ((field P) \/ (dom R)) \/ (rng R) by XBOOLE_1:4
.= (field P) \/ (field R) by XBOOLE_1:4 ; :: thesis: verum