let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I
for p, q being FinSequence of FreeAtoms H
for s, t being Element of (FreeProduct H) st s = Class ((EqCl (ReductionRel H)),p) & t = Class ((EqCl (ReductionRel H)),q) holds
s * t = Class ((EqCl (ReductionRel H)),(p ^ q))
let H be Group-like associative multMagma-Family of I; :: thesis: for p, q being FinSequence of FreeAtoms H
for s, t being Element of (FreeProduct H) st s = Class ((EqCl (ReductionRel H)),p) & t = Class ((EqCl (ReductionRel H)),q) holds
s * t = Class ((EqCl (ReductionRel H)),(p ^ q))
let p, q be FinSequence of FreeAtoms H; :: thesis: for s, t being Element of (FreeProduct H) st s = Class ((EqCl (ReductionRel H)),p) & t = Class ((EqCl (ReductionRel H)),q) holds
s * t = Class ((EqCl (ReductionRel H)),(p ^ q))
let s, t be Element of (FreeProduct H); :: thesis: ( s = Class ((EqCl (ReductionRel H)),p) & t = Class ((EqCl (ReductionRel H)),q) implies s * t = Class ((EqCl (ReductionRel H)),(p ^ q)) )
set R = EqCl (ReductionRel H);
assume A1: ( s = Class ((EqCl (ReductionRel H)),p) & t = Class ((EqCl (ReductionRel H)),q) ) ; :: thesis: s * t = Class ((EqCl (ReductionRel H)),(p ^ q))
( p in (FreeAtoms H) * & q in (FreeAtoms H) * ) by FINSEQ_1:def 11;
then reconsider v = p, w = q as Element of ((FreeAtoms H) *+^+<0>) by MONOID_0:61;
reconsider x = s, y = t as Element of Class (EqCl (ReductionRel H)) ;
thus s * t = Class ((EqCl (ReductionRel H)),(v * w)) by A1, ALGSTR_4:def 4
.= Class ((EqCl (ReductionRel H)),(p ^ q)) by MONOID_0:62 ; :: thesis: verum