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