A1: ( not X is empty implies ex f being BinOp of (free_magma_carrier X) st
for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
f . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] )

proof

assume A2: not X is empty ; :: thesis: ex f being BinOp of (free_magma_carrier X) st
for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
f . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)]
defpred S<sub>1</sub>[ set , set , set ] means for n, m being Nat st n = $1 `2 & m = $2 `2 holds
$3 = [[[($1 `1),($2 `1)],($1 `2)],(n + m)];
reconsider Y = free_magma_carrier X as non empty set by A2;
A3: for x, y being Element of Y ex z being Element of Y st S₁[x,y,z]

proof

let x, y be Element of Y; :: thesis: ex z being Element of Y st S₁[x,y,z]
reconsider X9 = X as non empty set by A2;
reconsider v = x as Element of free_magma_carrier X9 ;
reconsider w = y as Element of free_magma_carrier X9 ;
reconsider z = [[[(v `1),(w `1)],(v `2)],((v `2) + (w `2))] as Element of Y by Th26;
take z ; :: thesis: S₁[x,y,z]
thus S₁[x,y,z] ; :: thesis: verum

end;

consider f being Function of [:Y,Y:],Y such that
A4: for x, y being Element of Y holds S₁[x,y,f . (x,y)] from BINOP_1:sch 3(A3);
reconsider f = f as BinOp of (free_magma_carrier X) ;
take f ; :: thesis: for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
f . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)]
thus for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
f . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] by A4; :: thesis: verum

end;

A5: ( X is empty implies ex f being BinOp of (free_magma_carrier X) st f = {} )

proof

assume A6: X is empty ; :: thesis: ex f being BinOp of (free_magma_carrier X) st f = {}
then A7: free_magma_carrier X = {} ;
{} c= [:{},{}:] ;
then reconsider f = {} as Relation of [:{},{}:],{} ;
( ( [:{},{}:] = {} implies {} = {} ) & dom f = [:{},{}:] ) ;
then reconsider f = {} as BinOp of {} ;
for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 & v in free_magma_carrier X & w in free_magma_carrier X holds
f . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] by A6;
hence ex f being BinOp of (free_magma_carrier X) st f = {} by A7; :: thesis: verum

end;

now :: thesis: for f1, f2 being BinOp of (free_magma_carrier X) holds
( ( not X is empty & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
f1 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
f2 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) implies f1 = f2 ) & ( X is empty & f1 = {} & f2 = {} implies ( ( for b₃ being BinOp of (free_magma_carrier X) holds verum ) & ( not X is empty implies ex b₃ being BinOp of (free_magma_carrier X) st
for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b₃ . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( X is empty implies ex b<sub>3</sub> being BinOp of (free_magma_carrier X) st b<sub>3</sub> = {} ) & ( for b<sub>3</sub>, b<sub>4</sub> being BinOp of (free_magma_carrier X) holds
( ( not X is empty & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b<sub>3</sub> . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b₄ . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) implies b₃ = b₄ ) & ( X is empty & b₃ = {} & b₄ = {} implies b₃ = b₄ ) ) ) ) ) )

let f1, f2 be BinOp of (free_magma_carrier X); :: thesis: ( ( not X is empty & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
f1 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
f2 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) implies f1 = f2 ) & ( X is empty & f1 = {} & f2 = {} implies ( ( for b₁ being BinOp of (free_magma_carrier X) holds verum ) & ( not X is empty implies ex b₁ being BinOp of (free_magma_carrier X) st
for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b₁ . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( X is empty implies ex b<sub>1</sub> being BinOp of (free_magma_carrier X) st b<sub>1</sub> = {} ) & ( for b<sub>1</sub>, b<sub>2</sub> being BinOp of (free_magma_carrier X) holds
( ( not X is empty & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b<sub>1</sub> . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b₂ . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) implies b<sub>1</sub> = b<sub>2</sub> ) & ( X is empty & b<sub>1</sub> = {} & b<sub>2</sub> = {} implies b<sub>1</sub> = b<sub>2</sub> ) ) ) ) ) )
thus ( not X is empty & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
f1 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
f2 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) implies f1 = f2 ) :: thesis: ( X is empty & f1 = {} & f2 = {} implies ( ( for b<sub>1</sub> being BinOp of (free_magma_carrier X) holds verum ) & ( not X is empty implies ex b<sub>1</sub> being BinOp of (free_magma_carrier X) st
for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b<sub>1</sub> . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( X is empty implies ex b₁ being BinOp of (free_magma_carrier X) st b₁ = {} ) & ( for b₁, b₂ being BinOp of (free_magma_carrier X) holds
( ( not X is empty & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b₁ . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b<sub>2</sub> . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) implies b₁ = b₂ ) & ( X is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) ) ) ) )

proof

assume A8: not X is empty ; :: thesis: ( ex v, w being Element of free_magma_carrier X ex n, m being Nat st
( n = v `2 & m = w `2 & not f1 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) or ex v, w being Element of free_magma_carrier X ex n, m being Nat st
( n = v `2 & m = w `2 & not f2 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) or f1 = f2 )
assume A9: for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
f1 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ; :: thesis: ( ex v, w being Element of free_magma_carrier X ex n, m being Nat st
( n = v `2 & m = w `2 & not f2 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) or f1 = f2 )
assume A10: for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
f2 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ; :: thesis: f1 = f2
for v, w being Element of free_magma_carrier X holds f1 . (v,w) = f2 . (v,w)

proof

let v, w be Element of free_magma_carrier X; :: thesis: f1 . (v,w) = f2 . (v,w)
set n = v `2 ;
set m = w `2 ;
reconsider n = v `2 , m = w `2 as Nat by A8;
thus f1 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] by A9
.= f2 . (v,w) by A10 ; :: thesis: verum

end;

hence f1 = f2 by BINOP_1:2; :: thesis: verum

end;

assume ( X is empty & f1 = {} & f2 = {} ) ; :: thesis: ( ( for b₁ being BinOp of (free_magma_carrier X) holds verum ) & ( not X is empty implies ex b₁ being BinOp of (free_magma_carrier X) st
for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b₁ . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( X is empty implies ex b<sub>1</sub> being BinOp of (free_magma_carrier X) st b<sub>1</sub> = {} ) & ( for b<sub>1</sub>, b<sub>2</sub> being BinOp of (free_magma_carrier X) holds
( ( not X is empty & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b<sub>1</sub> . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b₂ . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) implies b<sub>1</sub> = b<sub>2</sub> ) & ( X is empty & b<sub>1</sub> = {} & b<sub>2</sub> = {} implies b<sub>1</sub> = b<sub>2</sub> ) ) ) )
hence ( ( for b<sub>1</sub> being BinOp of (free_magma_carrier X) holds verum ) & ( not X is empty implies ex b<sub>1</sub> being BinOp of (free_magma_carrier X) st
for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b<sub>1</sub> . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( X is empty implies ex b₁ being BinOp of (free_magma_carrier X) st b₁ = {} ) & ( for b₁, b₂ being BinOp of (free_magma_carrier X) holds
( ( not X is empty & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b₁ . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b<sub>2</sub> . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) implies b₁ = b₂ ) & ( X is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) ) ) ) ; :: thesis: verum

end;

hence ( ( for b₁ being BinOp of (free_magma_carrier X) holds verum ) & ( not X is empty implies ex b₁ being BinOp of (free_magma_carrier X) st
for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b₁ . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( X is empty implies ex b<sub>1</sub> being BinOp of (free_magma_carrier X) st b<sub>1</sub> = {} ) & ( for b<sub>1</sub>, b<sub>2</sub> being BinOp of (free_magma_carrier X) holds
( ( not X is empty & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b<sub>1</sub> . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b₂ . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) implies b₁ = b₂ ) & ( X is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) ) ) ) by A1, A5; :: thesis: verum