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

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

hence
f1 = f2
by FUNCT_2:12; :: thesis: verum
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;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