let R, S be Relation; :: thesis: for F being Function st F is_isomorphism_of R,S holds

for a, b being object st [a,b] in R & a <> b holds

( [(F . a),(F . b)] in S & F . a <> F . b )

let F be Function; :: thesis: ( F is_isomorphism_of R,S implies for a, b being object st [a,b] in R & a <> b holds

( [(F . a),(F . b)] in S & F . a <> F . b ) )

assume A1: F is_isomorphism_of R,S ; :: thesis: for a, b being object st [a,b] in R & a <> b holds

( [(F . a),(F . b)] in S & F . a <> F . b )

then A2: ( dom F = field R & F is one-to-one ) ;

let a, b be object ; :: thesis: ( [a,b] in R & a <> b implies ( [(F . a),(F . b)] in S & F . a <> F . b ) )

assume that

A3: [a,b] in R and

A4: a <> b ; :: thesis: ( [(F . a),(F . b)] in S & F . a <> F . b )

( a in field R & b in field R ) by A1, A3;

hence ( [(F . a),(F . b)] in S & F . a <> F . b ) by A1, A2, A3, A4; :: thesis: verum

for a, b being object st [a,b] in R & a <> b holds

( [(F . a),(F . b)] in S & F . a <> F . b )

let F be Function; :: thesis: ( F is_isomorphism_of R,S implies for a, b being object st [a,b] in R & a <> b holds

( [(F . a),(F . b)] in S & F . a <> F . b ) )

assume A1: F is_isomorphism_of R,S ; :: thesis: for a, b being object st [a,b] in R & a <> b holds

( [(F . a),(F . b)] in S & F . a <> F . b )

then A2: ( dom F = field R & F is one-to-one ) ;

let a, b be object ; :: thesis: ( [a,b] in R & a <> b implies ( [(F . a),(F . b)] in S & F . a <> F . b ) )

assume that

A3: [a,b] in R and

A4: a <> b ; :: thesis: ( [(F . a),(F . b)] in S & F . a <> F . b )

( a in field R & b in field R ) by A1, A3;

hence ( [(F . a),(F . b)] in S & F . a <> F . b ) by A1, A2, A3, A4; :: thesis: verum