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 A6:
P ~ = (R ~) | (dom (P ~))
; :: thesis: P = (rng P) |` Rassume A1:
P = (rng P) |` R
; :: thesis: P ~ = (R ~) | (dom (P ~))

end;now :: thesis: for x, y being object holds

( ( [x,y] in P ~ implies [x,y] in (R ~) | (dom (P ~)) ) & ( [x,y] in (R ~) | (dom (P ~)) implies [x,y] in P ~ ) )

hence
P ~ = (R ~) | (dom (P ~))
; :: thesis: verum( ( [x,y] in P ~ implies [x,y] in (R ~) | (dom (P ~)) ) & ( [x,y] in (R ~) | (dom (P ~)) implies [x,y] in P ~ ) )

let x, y be object ; :: thesis: ( ( [x,y] in P ~ implies [x,y] in (R ~) | (dom (P ~)) ) & ( [x,y] in (R ~) | (dom (P ~)) implies [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:20;

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;hereby :: thesis: ( [x,y] in (R ~) | (dom (P ~)) implies [x,y] in P ~ )

assume A4:
[x,y] in (R ~) | (dom (P ~))
; :: thesis: [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, XTUPLE_0:def 12;

hence [x,y] in (R ~) | (dom (P ~)) by A3, RELAT_1:def 11; :: thesis: verum

end;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, XTUPLE_0:def 12;

hence [x,y] in (R ~) | (dom (P ~)) by A3, RELAT_1:def 11; :: thesis: verum

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:20;

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

now :: thesis: for x, y being object holds

( ( [x,y] in P implies [x,y] in (rng P) |` R ) & ( [x,y] in (rng P) |` R implies [x,y] in P ) )

hence
P = (rng P) |` R
; :: thesis: verum( ( [x,y] in P implies [x,y] in (rng P) |` R ) & ( [x,y] in (rng P) |` R implies [x,y] in P ) )

let x, y be object ; :: thesis: ( ( [x,y] in P implies [x,y] in (rng P) |` R ) & ( [x,y] in (rng P) |` R implies [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:20;

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;hereby :: thesis: ( [x,y] in (rng P) |` R implies [x,y] in P )

assume A9:
[x,y] in (rng P) |` R
; :: thesis: [x,y] in Passume
[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:20;

hence [x,y] in (rng P) |` R by A8, RELAT_1:def 12; :: thesis: verum

end;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:20;

hence [x,y] in (rng P) |` R by A8, RELAT_1:def 12; :: thesis: verum

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:20;

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