let R be non empty RelStr ; :: thesis: (R,R)

set f = id the carrier of R;

reconsider f = id the carrier of R as Function of R,R ;

take f ; :: according to NECKLACE:def 1 :: thesis: ( f is one-to-one & ( for x, y being Element of R holds

( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R ) ) )

thus f is V7() ; :: thesis: for x, y being Element of R holds

( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R )

let x, y be Element of R; :: thesis: ( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R )

thus ( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R ) ; :: thesis: verum

set f = id the carrier of R;

reconsider f = id the carrier of R as Function of R,R ;

take f ; :: according to NECKLACE:def 1 :: thesis: ( f is one-to-one & ( for x, y being Element of R holds

( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R ) ) )

thus f is V7() ; :: thesis: for x, y being Element of R holds

( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R )

let x, y be Element of R; :: thesis: ( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R )

thus ( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R ) ; :: thesis: verum