consider A being non empty set , a being BinOp of A, Z being Element of A, r being Function of [:A, the carrier of FS:],A;
take RightModStr(# A,a,Z,r #) ; :: thesis: not RightModStr(# A,a,Z,r #) is empty
thus not the carrier of RightModStr(# A,a,Z,r #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum