let A, B be non empty AltGraph ; :: thesis: for F being BimapStr over 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 over 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 2,FUNCTOR0:def 13 :: 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 V7() ; :: according to FUNCTOR0:def 6 :: thesis: for a, b being Object of A st F . a = F . b holds

a = b

then [:f,f:] is V7() by A1, FUNCTOR0:9;

then A2: f is one-to-one by FUNCTOR0:7;

let a, b be Object of A; :: thesis: ( F . a = F . b implies a = b )

assume A3: F . a = F . b ; :: thesis: a = b

A4: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def 1;

[b,b] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

then the ObjectMap of F . (b,b) = [:f,f:] . (b,b) by A1, A4, FUNCT_4:43;

then A5: the ObjectMap of F . (b,b) = [(f . b),(f . b)] by FUNCT_3:75;

[a,a] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

then the ObjectMap of F . (a,a) = [:f,f:] . (a,a) by A1, A4, FUNCT_4:43;

then A6: the ObjectMap of F . (a,a) = [(f . a),(f . a)] by FUNCT_3:75;

( [(f . a),(f . a)] `1 = f . a & [(f . b),(f . b)] `1 = f . b ) ;

hence a = b by A2, A3, A6, A5, FUNCT_2:19; :: thesis: verum

for a, b being Object of A st F . a = F . b holds

a = b

let F be BimapStr over 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 2,FUNCTOR0:def 13 :: 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 V7() ; :: according to FUNCTOR0:def 6 :: thesis: for a, b being Object of A st F . a = F . b holds

a = b

then [:f,f:] is V7() by A1, FUNCTOR0:9;

then A2: f is one-to-one by FUNCTOR0:7;

let a, b be Object of A; :: thesis: ( F . a = F . b implies a = b )

assume A3: F . a = F . b ; :: thesis: a = b

A4: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def 1;

[b,b] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

then the ObjectMap of F . (b,b) = [:f,f:] . (b,b) by A1, A4, FUNCT_4:43;

then A5: the ObjectMap of F . (b,b) = [(f . b),(f . b)] by FUNCT_3:75;

[a,a] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

then the ObjectMap of F . (a,a) = [:f,f:] . (a,a) by A1, A4, FUNCT_4:43;

then A6: the ObjectMap of F . (a,a) = [(f . a),(f . a)] by FUNCT_3:75;

( [(f . a),(f . a)] `1 = f . a & [(f . b),(f . b)] `1 = f . b ) ;

hence a = b by A2, A3, A6, A5, FUNCT_2:19; :: thesis: verum