let G be strict Group; for x, y being Element of (InnAutGroup G)
for f, g being Element of InnAut G st x = f & y = g holds
x * y = f * g
let x, y be Element of (InnAutGroup G); for f, g being Element of InnAut G st x = f & y = g holds
x * y = f * g
let f, g be Element of InnAut G; ( x = f & y = g implies x * y = f * g )
( x is Element of (AutGroup G) & y is Element of (AutGroup G) )
by GROUP_2:42;
then consider x1, y1 being Element of (AutGroup G) such that
A1:
( x1 = x & y1 = y )
;
( f is Element of Aut G & g is Element of Aut G )
by Th12;
then consider f1, g1 being Element of Aut G such that
A2:
( f1 = f & g1 = g )
;
assume
( x = f & y = g )
; x * y = f * g
then
x1 * y1 = f1 * g1
by A2, A1, Def2;
hence
x * y = f * g
by A2, A1, GROUP_2:43; verum