set X1 = [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:];
defpred S₁[ object , object ] means 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 $1 = x & y = (x `1) `1 & z = (x `1) `2 holds
$2 = (f . y) * (g . z);
A1: for x being object st x in [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:] holds
ex y being object st
( y in the carrier of M & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:] implies ex y being object st
( y in the carrier of M & S₁[x,y] ) )
assume x in [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:] ; :: thesis: ex y being object st
( y in the carrier of M & S₁[x,y] )
then A2: x `1 in [:(free_magma (X,n)),(free_magma (X,m)):] by MCART_1:10;
then reconsider x1 = (x `1) `1 as Element of free_magma (X,n) by MCART_1:10;
reconsider x2 = (x `1) `2 as Element of free_magma (X,m) by A2, MCART_1:10;
set y = (f . x1) * (g . x2);
take (f . x1) * (g . x2) ; :: thesis: ( (f . x1) * (g . x2) in the carrier of M & S₁[x,(f . x1) * (g . x2)] )
thus (f . x1) * (g . x2) in the carrier of M ; :: thesis: S₁[x,(f . x1) * (g . x2)]
thus S₁[x,(f . x1) * (g . x2)] ; :: thesis: verum

end;

consider h being Function of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:], the carrier of M such that
A3: for x being object st x in [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:] holds
S₁[x,h . x] from FUNCT_2:sch 1(A1);
take h ; :: 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
h . x = (f . y) * (g . z)
thus 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
h . x = (f . y) * (g . z) by A3; :: thesis: verum