let F1, F2 be covariant Functor of (OrdC 2),C; :: thesis: ( ( for g being morphism of (OrdC 2) st not g is identity holds

F1 . g = f ) & ( for g being morphism of (OrdC 2) st not g is identity holds

F2 . g = f ) implies F1 = F2 )

assume A40: for g being morphism of (OrdC 2) st not g is identity holds

F1 . g = f ; :: thesis: ( ex g being morphism of (OrdC 2) st

( not g is identity & not F2 . g = f ) or F1 = F2 )

assume A41: for g being morphism of (OrdC 2) st not g is identity holds

F2 . g = f ; :: thesis: F1 = F2

consider f1 being morphism of (OrdC 2) such that

A42: not f1 is identity and

Ob (OrdC 2) = {(dom f1),(cod f1)} and

A43: Mor (OrdC 2) = {(dom f1),(cod f1),f1} by Th39;

for x being object st x in the carrier of (OrdC 2) holds

F1 . x = F2 . x

F1 . g = f ) & ( for g being morphism of (OrdC 2) st not g is identity holds

F2 . g = f ) implies F1 = F2 )

assume A40: for g being morphism of (OrdC 2) st not g is identity holds

F1 . g = f ; :: thesis: ( ex g being morphism of (OrdC 2) st

( not g is identity & not F2 . g = f ) or F1 = F2 )

assume A41: for g being morphism of (OrdC 2) st not g is identity holds

F2 . g = f ; :: thesis: F1 = F2

consider f1 being morphism of (OrdC 2) such that

A42: not f1 is identity and

Ob (OrdC 2) = {(dom f1),(cod f1)} and

A43: Mor (OrdC 2) = {(dom f1),(cod f1),f1} by Th39;

for x being object st x in the carrier of (OrdC 2) holds

F1 . x = F2 . x

proof

hence
F1 = F2
by FUNCT_2:12; :: thesis: verum
let x be object ; :: thesis: ( x in the carrier of (OrdC 2) implies F1 . x = F2 . x )

assume x in the carrier of (OrdC 2) ; :: thesis: F1 . x = F2 . x

then A44: x in {(dom f1),(cod f1),f1} by A43, CAT_6:def 1;

A45: F1 . f1 = f by A40, A42

.= F2 . f1 by A41, A42 ;

end;assume x in the carrier of (OrdC 2) ; :: thesis: F1 . x = F2 . x

then A44: x in {(dom f1),(cod f1),f1} by A43, CAT_6:def 1;

A45: F1 . f1 = f by A40, A42

.= F2 . f1 by A41, A42 ;