let G be 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