let R be Relation of ((FreeAtoms G) *+^+<0>); :: thesis: ( R = ReductionRel G iff for p, q being FinSequence of FreeAtoms G holds
( [p,q] in R iff ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I st
( p = (s ^ <*[i,(1_ (G . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex g, h being Element of (G . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) ) )
defpred S₁[ object , object ] means ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I st
( $1 = (s ^ <*[i,(1_ (G . i))]*>) ^ t & $2 = s ^ t ) or ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex g, h being Element of (G . i) st
( $1 = (s ^ <*[i,g],[i,h]*>) ^ t & $2 = (s ^ <*[i,(g * h)]*>) ^ t ) );
thus ( R = ReductionRel G implies for p, q being FinSequence of FreeAtoms G holds
( [p,q] in R iff S₁[p,q] ) ) :: thesis: ( ( for p, q being FinSequence of FreeAtoms G holds
( [p,q] in R iff ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I st
( p = (s ^ <*[i,(1_ (G . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex g, h being Element of (G . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) ) ) implies R = ReductionRel G )

proof

assume R = ReductionRel G ; :: thesis: for p, q being FinSequence of FreeAtoms G holds
( [p,q] in R iff S₁[p,q] )
then consider I9 being non empty set , G9 being Group-like multMagma-Family of I9 such that
A1: ( 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 Def2;
thus for p, q being FinSequence of FreeAtoms G holds
( [p,q] in R iff S₁[p,q] ) by A1; :: thesis: verum

end;

assume for p, q being FinSequence of FreeAtoms G holds
( [p,q] in R iff S₁[p,q] ) ; :: thesis: R = ReductionRel G
hence R = ReductionRel G by Def2; :: thesis: verum