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 )

( 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 ) ; :: thesis: x * y = f * g

then x1 * y1 = f1 * g1 by A2, A1, Def2;

hence x * y = f * g by A2, A1, GROUP_2:43; :: thesis: verum

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 )

( 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 ) ; :: thesis: x * y = f * g

then x1 * y1 = f1 * g1 by A2, A1, Def2;

hence x * y = f * g by A2, A1, GROUP_2:43; :: thesis: verum