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