let Q be multLoop; :: thesis: for f being Function of Q,Q holds
( f in InnAut Q iff ( f in Mlt ([#] Q) & f . (1. Q) = 1. Q ) )
let f be Function of Q,Q; :: thesis: ( f in InnAut Q iff ( f in Mlt ([#] Q) & f . (1. Q) = 1. Q ) )
thus ( f in InnAut Q implies ( f in Mlt ([#] Q) & f . (1. Q) = 1. Q ) ) :: thesis: ( f in Mlt ([#] Q) & f . (1. Q) = 1. Q implies f in InnAut Q )

proof

assume f in InnAut Q ; :: thesis: ( f in Mlt ([#] Q) & f . (1. Q) = 1. Q )
then ex g being Function of Q,Q st
( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) by Def49;
hence ( f in Mlt ([#] Q) & f . (1. Q) = 1. Q ) ; :: thesis: verum

end;

thus ( f in Mlt ([#] Q) & f . (1. Q) = 1. Q implies f in InnAut Q ) by Def49; :: thesis: verum