let R be Relation; :: thesis: field (R [*]) c= field R
set RR = R [*] ;
set LH = field (R [*]);
set RH = field R;

now

let x be set ; :: thesis: ( x in field (R [*]) implies b₁ in field R )
assume Z0: x in field (R [*]) ; :: thesis: b₁ in field R

per cases ( x in dom (R [*]) or x in rng (R [*]) ) by Z0, XBOOLE_0:def 3;

suppose x in dom (R [*]) ; :: thesis: b₁ in field R

then consider y being set such that
D0: [x,y] in R [*] by RELAT_1:def 4;
thus x in field R by D0, FINSEQ_1:def 16; :: thesis: verum

end;

suppose x in rng (R [*]) ; :: thesis: b₁ in field R

then consider y being set such that
D0: [y,x] in R [*] by RELAT_1:def 5;
thus x in field R by D0, FINSEQ_1:def 16; :: thesis: verum

end;

end;

end;

hence field (R [*]) c= field R by TARSKI:def 3; :: thesis: verum