let P, R be Relation; :: thesis: ( P = (rng P) | R iff P ~ = (R ~ ) | (dom (P ~ )) )

hereby :: thesis: ( P ~ = (R ~ ) | (dom (P ~ )) implies P = (rng P) | R )

assume A1: P = (rng P) | R ; :: thesis: P ~ = (R ~ ) | (dom (P ~ ))

now

let x, y be set ; :: thesis: ( ( [x,y] in P ~ implies [x,y] in (R ~ ) | (dom (P ~ )) ) & ( [x,y] in (R ~ ) | (dom (P ~ )) implies [x,y] in P ~ ) )

hereby :: thesis: ( [x,y] in (R ~ ) | (dom (P ~ )) implies [x,y] in P ~ )

assume A2: [x,y] in P ~ ; :: thesis: [x,y] in (R ~ ) | (dom (P ~ ))
then [y,x] in P by RELAT_1:def 7;
then [y,x] in R by A1, RELAT_1:def 12;
then A3: [x,y] in R ~ by RELAT_1:def 7;
x in dom (P ~ ) by A2, RELAT_1:def 4;
hence [x,y] in (R ~ ) | (dom (P ~ )) by A3, RELAT_1:def 11; :: thesis: verum

end;

assume A4: [x,y] in (R ~ ) | (dom (P ~ )) ; :: thesis: [x,y] in P ~
then [x,y] in R ~ by RELAT_1:def 11;
then A5: [y,x] in R by RELAT_1:def 7;
x in dom (P ~ ) by A4, RELAT_1:def 11;
then x in rng P by RELAT_1:37;
then [y,x] in (rng P) | R by A5, RELAT_1:def 12;
hence [x,y] in P ~ by A1, RELAT_1:def 7; :: thesis: verum

end;

hence P ~ = (R ~ ) | (dom (P ~ )) by RELAT_1:def 2; :: thesis: verum

end;

assume A6: P ~ = (R ~ ) | (dom (P ~ )) ; :: thesis: P = (rng P) | R

now

let x, y be set ; :: thesis: ( ( [x,y] in P implies [x,y] in (rng P) | R ) & ( [x,y] in (rng P) | R implies [x,y] in P ) )

hereby :: thesis: ( [x,y] in (rng P) | R implies [x,y] in P )

assume [x,y] in P ; :: thesis: [x,y] in (rng P) | R
then A7: [y,x] in P ~ by RELAT_1:def 7;
then [y,x] in R ~ by A6, RELAT_1:def 11;
then A8: [x,y] in R by RELAT_1:def 7;
y in dom (P ~ ) by A6, A7, RELAT_1:def 11;
then y in rng P by RELAT_1:37;
hence [x,y] in (rng P) | R by A8, RELAT_1:def 12; :: thesis: verum

end;

assume A9: [x,y] in (rng P) | R ; :: thesis: [x,y] in P
then [x,y] in R by RELAT_1:def 12;
then A10: [y,x] in R ~ by RELAT_1:def 7;
y in rng P by A9, RELAT_1:def 12;
then y in dom (P ~ ) by RELAT_1:37;
then [y,x] in (R ~ ) | (dom (P ~ )) by A10, RELAT_1:def 11;
hence [x,y] in P by A6, RELAT_1:def 7; :: thesis: verum

end;

hence P = (rng P) | R by RELAT_1:def 2; :: thesis: verum