let R1, R2 be Relation of ((FreeAtoms G) *+^+<0>); :: thesis: ( ( I is empty implies R1 = {} ) & ( 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 R1 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 ) ) ) ) ) ) & ( I is empty implies R2 = {} ) & ( 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 R2 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 ) ) ) ) ) ) implies R1 = R2 )
assume that
A5: ( ( I is empty implies R1 = {} ) & ( 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 R1 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 ) ) ) ) ) ) ) and
A6: ( ( I is empty implies R2 = {} ) & ( 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 R2 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 ) ) ) ) ) ) ) ; :: thesis: R1 = R2

per cases ( not I is empty or I is empty ) ;

suppose not I is empty ; :: thesis: R1 = R2

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>);
A7: for p, q being Element of the carrier of ((FreeAtoms G) *+^+<0>) holds
( [p,q] in R1 iff S₁[p,q] )

proof

let p, q be Element of the carrier of ((FreeAtoms G) *+^+<0>); :: thesis: ( [p,q] in R1 iff S₁[p,q] )
( p in the carrier of ((FreeAtoms G) *+^+<0>) & q in the carrier of ((FreeAtoms G) *+^+<0>) ) ;
then ( p in (FreeAtoms G) * & q in (FreeAtoms G) * ) by MONOID_0:61;
then ( p is FinSequence of FreeAtoms G & q is FinSequence of FreeAtoms G ) by FINSEQ_1:def 11;
hence ( [p,q] in R1 iff S₁[p,q] ) by A5; :: thesis: verum

end;

A8: for p, q being Element of the carrier of ((FreeAtoms G) *+^+<0>) holds
( [p,q] in R2 iff S₁[p,q] )

proof

let p, q be Element of the carrier of ((FreeAtoms G) *+^+<0>); :: thesis: ( [p,q] in R2 iff S₁[p,q] )
( p in the carrier of ((FreeAtoms G) *+^+<0>) & q in the carrier of ((FreeAtoms G) *+^+<0>) ) ;
then ( p in (FreeAtoms G) * & q in (FreeAtoms G) * ) by MONOID_0:61;
then ( p is FinSequence of FreeAtoms G & q is FinSequence of FreeAtoms G ) by FINSEQ_1:def 11;
hence ( [p,q] in R2 iff S₁[p,q] ) by A6; :: thesis: verum

end;

thus R1 = R2 from RELSET_1:sch 4(A7, A8); :: thesis: verum

end;

suppose I is empty ; :: thesis: R1 = R2

hence R1 = R2 by A5, A6; :: thesis: verum

end;

end;