let G be strict Group; :: thesis: 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); :: thesis: 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; :: thesis: ( x = f & y = g implies x * y = f * g )
assume A1: ( x = f & y = g ) ; :: thesis: x * y = f * g
( f is Element of Aut G & g is Element of Aut G ) by Th13;
then consider f1, g1 being Element of Aut G such that
A2: ( f1 = f & g1 = g ) ;
( x is Element of (AutGroup G) & y is Element of (AutGroup G) ) by GROUP_2:51;
then consider x1, y1 being Element of (AutGroup G) such that
A3: ( x1 = x & y1 = y ) ;
x1 * y1 = f1 * g1 by A1, A2, A3, Def2;
hence x * y = f * g by A2, A3, GROUP_2:52; :: thesis: verum