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

A1: now

let a, b be set ; :: 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:30; :: thesis: [((id (field R)) . a),((id (field R)) . b)] in R
then (id (field R)) . a = a by FUNCT_1:35;
hence [((id (field R)) . a),((id (field R)) . b)] in R by A2, A3, FUNCT_1:35; :: 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:35;
hence [a,b] in R by A5, FUNCT_1:35; :: thesis: verum

end;

( dom (id (field R)) = field R & rng (id (field R)) = field R ) by RELAT_1:71;
hence id (field R) is_isomorphism_of R,R by A1, Def7; :: thesis: verum