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
A3: for o being object of A holds X . o = s ! (F . o) and
A4: for o being object of A holds Y . o = s ! (F . o) ; :: thesis: X = Y
A5: G1 * F is_transformable_to G2 * F by B1, 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 A5, FUNCTOR2:def 4
.= s ! (F . o) by A3
.= Y . o by A4
.= Y ! o by A5, FUNCTOR2:def 4 ; :: thesis: verum

end;

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