let R be Relation; :: thesis: field R = field (R ~)
thus field R = (rng (R ~)) \/ (rng R) by Th14
.= field (R ~) by Th14 ; :: thesis: verum