let R, S be Relation; :: thesis: for F being Function st F is_isomorphism_of R,S holds
for a, b being set 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 set 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 set st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in S & F . a <> F . b )
then A2: ( dom F = field R & rng F = field S & F is one-to-one & ( for a, b being set holds
( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ) ) by Def7;
let a, b be set ; :: thesis: ( [a,b] in R & a <> b implies ( [(F . a),(F . b)] in S & F . a <> F . b ) )
assume A3: ( [a,b] in R & a <> b ) ; :: thesis: ( [(F . a),(F . b)] in S & F . a <> F . b )
then ( a in field R & b in field R & [(F . a),(F . b)] in S ) by A1, Def7;
hence ( [(F . a),(F . b)] in S & F . a <> F . b ) by A2, A3, FUNCT_1:def 8; :: thesis: verum