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 Th74;
card G = 1 by Th11;
then card H = 1 by A1, Th73;
hence H is trivial by Th11; :: thesis: verum