then reconsider I9 = I as non empty set ;
reconsider G9 = G as Group-like multMagma-Family of I9 ;
defpred S₁[ object , object ] means ( ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 st
( $1 = (s ^ <*[i,(1_ (G9 . i))]*>) ^ t & $2 = s ^ t ) or ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 ex g, h being Element of (G9 . i) st
( $1 = (s ^ <*[i,g],[i,h]*>) ^ t & $2 = (s ^ <*[i,(g * h)]*>) ^ t ) );
set C = the carrier of ((FreeAtoms G) *+^+<0>);
consider R being Relation of ((FreeAtoms G) *+^+<0>) such that
A2: for x, y being object holds
( [x,y] in R iff ( x in the carrier of ((FreeAtoms G) *+^+<0>) & y in the carrier of ((FreeAtoms G) *+^+<0>) & S₁[x,y] ) ) from RELSET_1:sch 1();
take R ; :: thesis:
thus ( I is empty implies R = {} ) by A1; :: thesis:
assume not I is empty ; :: thesis:
take I9 ; :: thesis:
take G9 ; :: thesis:
thus ( I = I9 & G = G9 ) ; :: thesis:
let p, q be FinSequence of FreeAtoms G9; :: thesis:
thus ( [p,q] in R implies S₁[p,q] ) by A2; :: thesis:
assume A3: S₁[p,q] ; :: thesis:
( p in (FreeAtoms G9) * & q in (FreeAtoms G9) * ) by FINSEQ_1:def 11;
then ( p in the carrier of ((FreeAtoms G) *+^+<0>) & q in the carrier of ((FreeAtoms G) *+^+<0>) ) by MONOID_0:61;
hence [p,q] in R by A2, A3; :: thesis:

end;

reconsider R = {} as Relation of ((FreeAtoms G) *+^+<0>) by RELSET_1:12;
take R ; :: thesis:
thus ( I is empty implies R = {} ) ; :: thesis:
thus ( not I is empty implies ex I9 being non empty set ex G9 being Group-like multMagma-Family of I9 st
( I = I9 & G = G9 & ( for p, q being FinSequence of FreeAtoms G9 holds
( [p,q] in R iff ( ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 st
( p = (s ^ <*[i,(1_ (G9 . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G9 ex i being Element of I9 ex g, h being Element of (G9 . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) ) ) ) ) by A4; :: thesis:

end;