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