let R be Relation; :: thesis: for f being Function st dom f c= dom R & R c= f holds
R = f
let f be Function; :: thesis: ( dom f c= dom R & R c= f implies R = f )
set X = dom f;
assume B4: ( dom f c= dom R & R c= f ) ; :: thesis: R = f
then B2: ( dom f c= dom R & dom R c= dom f ) by RELAT_1:11;
then B3: dom f = dom R by XBOOLE_0:def 10;
reconsider RR = R as dom f -defined Relation by B2, RELAT_1:def 18;
reconsider P = RR as dom f -defined total Relation by B3, PARTFUN1:def 2;
consider g being Function of (dom f),(rng P) such that
B0: ( g c= P & dom g = dom f ) by Lm46;
f c= R by B0, B4, GRFUNC_1:3, XBOOLE_1:1;
hence R = f by B4, XBOOLE_0:def 10; :: thesis: verum