let I be non empty set ; :: thesis: for G being Group-like multMagma-Family of I holds
( dom (ReductionRel G) c= (FreeAtoms G) * & rng (ReductionRel G) = (FreeAtoms G) * & field (ReductionRel G) = (FreeAtoms G) * )
let G be Group-like multMagma-Family of I; :: thesis: ( dom (ReductionRel G) c= (FreeAtoms G) * & rng (ReductionRel G) = (FreeAtoms G) * & field (ReductionRel G) = (FreeAtoms G) * )
dom (ReductionRel G) c= the carrier of ((FreeAtoms G) *+^+<0>) ;
hence A1: dom (ReductionRel G) c= (FreeAtoms G) * by MONOID_0:61; :: thesis: ( rng (ReductionRel G) = (FreeAtoms G) * & field (ReductionRel G) = (FreeAtoms G) * )
rng (ReductionRel G) c= the carrier of ((FreeAtoms G) *+^+<0>) ;
then A2: rng (ReductionRel G) c= (FreeAtoms G) * by MONOID_0:61;

now :: thesis: for x being object st x in (FreeAtoms G) * holds
x in rng (ReductionRel G)

let x be object ; :: thesis: ( x in (FreeAtoms G) * implies x in rng (ReductionRel G) )
assume x in (FreeAtoms G) * ; :: thesis: x in rng (ReductionRel G)
then reconsider p = x as FinSequence of FreeAtoms G by FINSEQ_1:def 11;
set q = <*> (FreeAtoms G);
set i = the Element of I;
[((p ^ <*[ the Element of I,(1_ (G . the Element of I))]*>) ^ (<*> (FreeAtoms G))),(p ^ (<*> (FreeAtoms G)))] in ReductionRel G by Th28;
then p ^ (<*> (FreeAtoms G)) in rng (ReductionRel G) by XTUPLE_0:def 13;
hence x in rng (ReductionRel G) by FINSEQ_1:34; :: thesis: verum

end;

then (FreeAtoms G) * c= rng (ReductionRel G) by TARSKI:def 3;
hence A3: rng (ReductionRel G) = (FreeAtoms G) * by A2, XBOOLE_0:def 10; :: thesis: field (ReductionRel G) = (FreeAtoms G) *
(dom (ReductionRel G)) \/ (rng (ReductionRel G)) = (FreeAtoms G) * by A1, A3, XBOOLE_1:12;
hence field (ReductionRel G) = (FreeAtoms G) * by RELAT_1:def 6; :: thesis: verum