set X1 = [:[:(free_magma X,n),(free_magma X,m):],{n}:];
defpred S₁[ set , set ] 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 set st x in [:[:(free_magma X,n),(free_magma X,m):],{n}:] holds
ex y being set st
( y in the carrier of M & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in [:[:(free_magma X,n),(free_magma X,m):],{n}:] implies ex y being set 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 set 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 set 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