let G be trivial strict Group; :: thesis: for H being strict Group st G,H are_isomorphic holds
H is trivial
let H be strict Group; :: thesis: ( G,H are_isomorphic implies H is trivial )
assume A1: G,H are_isomorphic ; :: thesis: H is trivial
then reconsider H = H as finite Group by Th85;
card G = 1 by Th12;
then card H = 1 by A1, Th84;
hence H is trivial by Th12; :: thesis: verum