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 ;
then A3: [x,y] in R ~ by RELAT_1:def 7;
x in dom (P ~) by ;
hence [x,y] in (R ~) | (dom (P ~)) by ; :: 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 ;
then x in rng P by RELAT_1:20;
then [y,x] in (rng P) |` R by ;
hence [x,y] in P ~ by ; :: 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 ;
then A8: [x,y] in R by RELAT_1:def 7;
y in dom (P ~) by ;
then y in rng P by RELAT_1:20;
hence [x,y] in (rng P) |` R by ; :: 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 ;
then y in dom (P ~) by RELAT_1:20;
then [y,x] in (R ~) | (dom (P ~)) by ;
hence [x,y] in P by ; :: thesis: verum
end;
hence P = (rng P) |` R ; :: thesis: verum