let R be Relation; :: thesis: id () 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 ()) . a),((id ()) . b)] in R ) ) & ( a in field R & b in field R & [((id ()) . a),((id ()) . 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 ()) . a),((id ()) . b)] in R ) ) & ( a in field R & b in field R & [((id ()) . a),((id ()) . b)] in R implies [a,b] in R ) )
thus ( [a,b] in R implies ( a in field R & b in field R & [((id ()) . a),((id ()) . b)] in R ) ) :: thesis: ( a in field R & b in field R & [((id ()) . a),((id ()) . 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 ()) . a),((id ()) . b)] in R )
hence A3: ( a in field R & b in field R ) by RELAT_1:15; :: thesis: [((id ()) . a),((id ()) . b)] in R
then (id ()) . a = a by FUNCT_1:18;
hence [((id ()) . a),((id ()) . b)] in R by ; :: thesis: verum
end;
assume that
A4: a in field R and
A5: ( b in field R & [((id ()) . a),((id ()) . b)] in R ) ; :: thesis: [a,b] in R
(id ()) . a = a by ;
hence [a,b] in R by ; :: thesis: verum
end;
thus id () is_isomorphism_of R,R by A1; :: thesis: verum