let X, Y be transformation of G * F1,G * F2; :: thesis: ( ( for o being Object of A holds X . o = G . (t ! o) ) & ( for o being Object of A holds Y . o = G . (t ! o) ) implies X = Y )
assume that
A4: for o being Object of A holds X . o = G . (t ! o) and
A5: for o being Object of A holds Y . o = G . (t ! o) ; :: thesis: X = Y
A6: G * F1 is_transformable_to G * F2 by A1, Th10;

now :: thesis: for o being Object of A holds X ! o = Y ! o

let o be Object of A; :: thesis: X ! o = Y ! o
thus X ! o = X . o by A6, FUNCTOR2:def 4
.= G . (t ! o) by A4
.= Y . o by A5
.= Y ! o by A6, FUNCTOR2:def 4 ; :: thesis: verum

end;

hence X = Y by A1, Th10, FUNCTOR2:3; :: thesis: verum