let R be Relation; :: thesis: id (field R) is_isomorphism_of R,R

A1: now :: thesis: for a, b being object holds
( ( [a,b] in R implies ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R ) ) & ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R implies [a,b] in R ) )

let a, b be object ; :: thesis: ( ( [a,b] in R implies ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R ) ) & ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R implies [a,b] in R ) )
thus ( [a,b] in R implies ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R ) ) :: thesis: ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R implies [a,b] in R )

proof

assume A2: [a,b] in R ; :: thesis: ( a in field R & b in field R & [((id (field R)) . a),((id (field R)) . b)] in R )
hence A3: ( a in field R & b in field R ) by RELAT_1:15; :: thesis: [((id (field R)) . a),((id (field R)) . b)] in R
then (id (field R)) . a = a by FUNCT_1:18;
hence [((id (field R)) . a),((id (field R)) . b)] in R by A2, A3, FUNCT_1:18; :: thesis: verum

end;

assume that
A4: a in field R and
A5: ( b in field R & [((id (field R)) . a),((id (field R)) . b)] in R ) ; :: thesis: [a,b] in R
(id (field R)) . a = a by A4, FUNCT_1:18;
hence [a,b] in R by A5, FUNCT_1:18; :: thesis: verum

end;

thus id (field R) is_isomorphism_of R,R by A1; :: thesis: verum