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 A1: ( dom f c= dom R & R c= f ) ; :: thesis: R = f
then A2: ( dom f c= dom R & dom R c= dom f ) by RELAT_1:11;
reconsider RR = R as dom f -defined Relation by RELAT_1:def 18, A1, RELAT_1:11;
reconsider P = RR as dom f -defined total Relation by PARTFUN1:def 2, A2, XBOOLE_0:def 10;
consider g being Function of (dom f),(rng P) such that
A3: ( g c= P & dom g = dom f ) by Lm41;
f c= R by GRFUNC_1:3, A3, A1, XBOOLE_1:1;
hence R = f by A1; :: thesis: verum