let X, Y be transformation of G1 * F,G2 * F; :: thesis: ( ( for o being object of A holds X . o = s ! (F . o) ) & ( for o being object of A holds Y . o = s ! (F . o) ) implies X = Y )
assume that
A5: for o being object of A holds X . o = s ! (F . o) and
A6: for o being object of A holds Y . o = s ! (F . o) ; :: thesis: X = Y
A7: G1 * F is_transformable_to G2 * F by A1, Th10;

now

let o be object of A; :: thesis: X ! o = Y ! o
thus X ! o = X . o by A7, FUNCTOR2:def 4
.= s ! (F . o) by A5
.= Y . o by A6
.= Y ! o by A7, FUNCTOR2:def 4 ; :: thesis: verum

end;

hence X = Y by A7, FUNCTOR2:5; :: thesis: verum