let A, B be non empty AltGraph ; :: thesis: for F being BimapStr of A,B st F is Contravariant & F is one-to-one holds
for a, b being object of A st F . a = F . b holds
a = b
let F be BimapStr of A,B; :: thesis: ( F is Contravariant & F is one-to-one implies for a, b being object of A st F . a = F . b holds
a = b )
given f being Function of the carrier of A,the carrier of B such that A1: the ObjectMap of F = ~ [:f,f:] ; :: according to FUNCTOR0:def 3,FUNCTOR0:def 14 :: thesis: ( not F is one-to-one or for a, b being object of A st F . a = F . b holds
a = b )
assume the ObjectMap of F is one-to-one ; :: according to FUNCTOR0:def 7 :: thesis: for a, b being object of A st F . a = F . b holds
a = b
then [:f,f:] is one-to-one by A1, FUNCTOR0:10;
then A2: f is one-to-one by FUNCTOR0:8;
let a, b be object of A; :: thesis: ( F . a = F . b implies a = b )
assume A3: F . a = F . b ; :: thesis: a = b
( dom the ObjectMap of F = [:the carrier of A,the carrier of A:] & [a,a] in [:the carrier of A,the carrier of A:] & [b,b] in [:the carrier of A,the carrier of A:] ) by FUNCT_2:def 1, ZFMISC_1:def 2;
then ( the ObjectMap of F . a,a = [:f,f:] . a,a & the ObjectMap of F . b,b = [:f,f:] . b,b ) by A1, FUNCT_4:44;
then A4: ( the ObjectMap of F . a,a = [(f . a),(f . a)] & the ObjectMap of F . b,b = [(f . b),(f . b)] ) by FUNCT_3:96;
( [(f . a),(f . a)] `1 = f . a & [(f . b),(f . b)] `1 = f . b ) by MCART_1:7;
hence a = b by A2, A3, A4, FUNCT_2:25; :: thesis: verum