let I be non empty set ; :: thesis: for G being Group-like multMagma-Family of I
for x, y being object st [x,y] in ReductionRel G holds
( x is FinSequence of FreeAtoms G & y is FinSequence of FreeAtoms G )
let G be Group-like multMagma-Family of I; :: thesis: for x, y being object st [x,y] in ReductionRel G holds
( x is FinSequence of FreeAtoms G & y is FinSequence of FreeAtoms G )
let x, y be object ; :: thesis: ( [x,y] in ReductionRel G implies ( x is FinSequence of FreeAtoms G & y is FinSequence of FreeAtoms G ) )
assume [x,y] in ReductionRel G ; :: thesis: ( x is FinSequence of FreeAtoms G & y is FinSequence of FreeAtoms G )
then ( x in field (ReductionRel G) & y in field (ReductionRel G) ) by RELAT_1:15;
then ( x in (FreeAtoms G) * & y in (FreeAtoms G) * ) by Th30;
hence ( x is FinSequence of FreeAtoms G & y is FinSequence of FreeAtoms G ) by FINSEQ_1:def 11; :: thesis: verum