let f1, f2 be Function of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:],M; :: thesis: ( ( for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
f1 . x = (f . y) * (g . z) ) & ( for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
f2 . x = (f . y) * (g . z) ) implies f1 = f2 )
assume A4: for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
f1 . x = (f . y) * (g . z) ; :: thesis: ( ex x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:] ex y being Element of free_magma (X,n) ex z being Element of free_magma (X,m) st
( y = (x `1) `1 & z = (x `1) `2 & not f2 . x = (f . y) * (g . z) ) or f1 = f2 )
assume A5: for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
f2 . x = (f . y) * (g . z) ; :: thesis: f1 = f2
for x being object st x in [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:] holds
f1 . x = f2 . x

proof

let x be object ; :: thesis: ( x in [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:] implies f1 . x = f2 . x )
assume x in [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:] ; :: thesis: f1 . x = f2 . x
then reconsider x9 = x as Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:] ;
A6: x9 `1 in [:(free_magma (X,n)),(free_magma (X,m)):] by MCART_1:10;
then reconsider x1 = (x9 `1) `1 as Element of free_magma (X,n) by MCART_1:10;
reconsider x2 = (x9 `1) `2 as Element of free_magma (X,m) by A6, MCART_1:10;
thus f1 . x = (f . x1) * (g . x2) by A4
.= f2 . x by A5 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:12; :: thesis: verum