let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds

for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 ! a = t2 ! a ) holds

t1 = t2

let F1, F2 be Functor of A,B; :: thesis: ( F1 is_transformable_to F2 implies for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 ! a = t2 ! a ) holds

t1 = t2 )

assume A1: F1 is_transformable_to F2 ; :: thesis: for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 ! a = t2 ! a ) holds

t1 = t2

let t1, t2 be transformation of F1,F2; :: thesis: ( ( for a being Object of A holds t1 ! a = t2 ! a ) implies t1 = t2 )

assume A2: for a being Object of A holds t1 ! a = t2 ! a ; :: thesis: t1 = t2

for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 ! a = t2 ! a ) holds

t1 = t2

let F1, F2 be Functor of A,B; :: thesis: ( F1 is_transformable_to F2 implies for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 ! a = t2 ! a ) holds

t1 = t2 )

assume A1: F1 is_transformable_to F2 ; :: thesis: for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 ! a = t2 ! a ) holds

t1 = t2

let t1, t2 be transformation of F1,F2; :: thesis: ( ( for a being Object of A holds t1 ! a = t2 ! a ) implies t1 = t2 )

assume A2: for a being Object of A holds t1 ! a = t2 ! a ; :: thesis: t1 = t2

now :: thesis: for a being object st a in the carrier of A holds

t1 . a = t2 . a

hence
t1 = t2
by PBOOLE:3; :: thesis: verumt1 . a = t2 . a

let a be object ; :: thesis: ( a in the carrier of A implies t1 . a = t2 . a )

assume a in the carrier of A ; :: thesis: t1 . a = t2 . a

then reconsider o = a as Object of A ;

thus t1 . a = t1 ! o by A1, Def4

.= t2 ! o by A2

.= t2 . a by A1, Def4 ; :: thesis: verum

end;assume a in the carrier of A ; :: thesis: t1 . a = t2 . a

then reconsider o = a as Object of A ;

thus t1 . a = t1 ! o by A1, Def4

.= t2 ! o by A2

.= t2 . a by A1, Def4 ; :: thesis: verum