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 :: 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 ~ ) )
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 ~ ) )
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, XTUPLE_0:def 12;
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: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;
hence P ~ = (R ~) | (dom (P ~)) ; :: thesis: verum
end;
assume A6: P ~ = (R ~) | (dom (P ~)) ; :: thesis: P = (rng P) |` R
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 ) )
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 ) )
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:20;
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: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;
hence P = (rng P) |` R ; :: thesis: verum