let O be set ; :: thesis: for G being strict Group ex H being strict GroupWithOperators of O st G = multMagma(# the carrier of H, the multF of H #)
let G be strict Group; :: thesis: ex H being strict GroupWithOperators of O st G = multMagma(# the carrier of H, the multF of H #)
consider H being non empty HGrWOpStr over O such that
A1: ( H is strict & H is distributive & H is Group-like & H is associative ) and
A2: G = multMagma(# the carrier of H, the multF of H #) by Lm2;
reconsider H = H as strict GroupWithOperators of O by A1;
take H ; :: thesis: G = multMagma(# the carrier of H, the multF of H #)
thus G = multMagma(# the carrier of H, the multF of H #) by A2; :: thesis: verum