set A = the non empty set ;
set m = the BinOp of the non empty set ;
set r = the Function of (n -tuples_on the non empty set ), the non empty set ;
take
ReperAlgebraStr(# the non empty set , the BinOp of the non empty set , the Function of (n -tuples_on the non empty set ), the non empty set #)
; not ReperAlgebraStr(# the non empty set , the BinOp of the non empty set , the Function of (n -tuples_on the non empty set ), the non empty set #) is empty
thus
not ReperAlgebraStr(# the non empty set , the BinOp of the non empty set , the Function of (n -tuples_on the non empty set ), the non empty set #) is empty
; verum