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 set st x in [:[:(free_magma X,n),(free_magma X,m):],{n}:] holds
f1 . x = f2 . x

proof

let x be set ; :: 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:18; :: thesis: verum