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
A4: for o being Object of A holds X . o = s ! (F . o) and
A5: for o being Object of A holds Y . o = s ! (F . o) ; :: thesis: X = Y
A6: G1 * F is_transformable_to G2 * F 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
.= s ! (F . 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