let I be non empty set ; :: thesis: for G being Group-like multMagma-Family of I holds {} is_a_normal_form_wrt ReductionRel G
let G be Group-like multMagma-Family of I; :: thesis: {} is_a_normal_form_wrt ReductionRel G

now :: thesis: for q being object holds not [(<*> (FreeAtoms G)),q] in ReductionRel G

set p = <*> (FreeAtoms G);
given q being object such that A1: [(<*> (FreeAtoms G)),q] in ReductionRel G ; :: thesis: contradiction
q in field (ReductionRel G) by A1, RELAT_1:15;
then q in (FreeAtoms G) * by Th30;
then reconsider q = q as FinSequence of FreeAtoms G by FINSEQ_1:def 11;
len (<*> (FreeAtoms G)) = (len q) + 1 by A1, Th35;
hence contradiction ; :: thesis: verum

end;

hence {} is_a_normal_form_wrt ReductionRel G by REWRITE1:def 5; :: thesis: verum