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 ) )

thus
id (field R) is_isomorphism_of R,R
by A1; :: thesis: verum( ( [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 )

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 ( [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 that
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;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

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