set I = InnAut Q;
thus A1: not InnAut Q is empty :: thesis: ( InnAut Q is composition-closed & InnAut Q is inverse-closed )

proof

set g = (curry the multF of Q) . (1. Q);
ex h being Function of Q,Q st
( (curry the multF of Q) . (1. Q) = h & h in Mlt ([#] Q) & h . (1. Q) = 1. Q )

proof

take (curry the multF of Q) . (1. Q) ; :: thesis: ( (curry the multF of Q) . (1. Q) = (curry the multF of Q) . (1. Q) & (curry the multF of Q) . (1. Q) in Mlt ([#] Q) & ((curry the multF of Q) . (1. Q)) . (1. Q) = 1. Q )
((curry the multF of Q) . (1. Q)) . (1. Q) = (1. Q) * (1. Q) by FUNCT_5:69
.= 1. Q ;
hence ( (curry the multF of Q) . (1. Q) = (curry the multF of Q) . (1. Q) & (curry the multF of Q) . (1. Q) in Mlt ([#] Q) & ((curry the multF of Q) . (1. Q)) . (1. Q) = 1. Q ) by Th32; :: thesis: verum

end;

hence not InnAut Q is empty by Def49; :: thesis: verum

end;

thus InnAut Q is composition-closed :: thesis: InnAut Q is inverse-closed

proof

let f, g be Element of InnAut Q; :: according to AIMLOOP:def 36 :: thesis: ( f in InnAut Q & g in InnAut Q implies f * g in InnAut Q )
consider f2 being Function of Q,Q such that
A5: ( f = f2 & f2 in Mlt ([#] Q) & f2 . (1. Q) = 1. Q ) by A1, Def49;
consider g2 being Function of Q,Q such that
A6: ( g = g2 & g2 in Mlt ([#] Q) & g2 . (1. Q) = 1. Q ) by A1, Def49;
set h = f2 * g2;
( f * g = f2 * g2 & f2 * g2 in Mlt ([#] Q) & (f2 * g2) . (1. Q) = 1. Q ) by A5, A6, FUNCT_2:15, Def34;
hence ( f in InnAut Q & g in InnAut Q implies f * g in InnAut Q ) by Def49; :: thesis: verum

end;

thus InnAut Q is inverse-closed :: thesis: verum

proof

let f be Element of InnAut Q; :: according to AIMLOOP:def 37 :: thesis: ( f in InnAut Q implies f " in InnAut Q )
consider f2 being Function of Q,Q such that
A7: ( f = f2 & f2 in Mlt ([#] Q) & f2 . (1. Q) = 1. Q ) by A1, Def49;
ex h being Function of Q,Q st
( f " = h & h in Mlt ([#] Q) & h . (1. Q) = 1. Q )

proof

reconsider f2 = f2 as Permutation of the carrier of Q by Th35, A7;
take f2 " ; :: thesis: ( f " = f2 " & f2 " in Mlt ([#] Q) & (f2 ") . (1. Q) = 1. Q )
(f2 ") . (1. Q) = ((f2 ") * f2) . (1. Q) by FUNCT_2:15, A7
.= (id the carrier of Q) . (1. Q) by FUNCT_2:61
.= 1. Q ;
hence ( f " = f2 " & f2 " in Mlt ([#] Q) & (f2 ") . (1. Q) = 1. Q ) by A7, Def35; :: thesis: verum

end;

hence ( f in InnAut Q implies f " in InnAut Q ) by Def49; :: thesis: verum

end;