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

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