let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G) st G is strict & G is trivial holds
phi = 1: (A,(AutGroup G))
let phi be Homomorphism of A,(AutGroup G); :: thesis: ( G is strict & G is trivial implies phi = 1: (A,(AutGroup G)) )
assume ( G is strict & G is trivial ) ; :: thesis: phi = 1: (A,(AutGroup G))
then AutGroup G is trivial by Th70;
hence phi = 1: (A,(AutGroup G)) by Th68; :: thesis: verum