let V be non empty addLoopStr ; :: thesis: for M being empty Subset of
for N being Subset of holds M + N = {}
let M be empty Subset of ; :: thesis: for N being Subset of holds M + N = {}
let N be Subset of ; :: thesis: M + N = {}
A1: M + N = { (u + v) where u, v is Element of : ( u in {} & v in N ) } by RUSUB_4:def 10;
for x being Element of st x in M + N holds
x in {}

proof

let x be Element of ; :: thesis: ( x in M + N implies x in {} )
assume x in M + N ; :: thesis: x in {}
then ex u, v being Element of st
( x = u + v & u in {} & v in N ) by A1;
hence x in {} ; :: thesis: verum

end;

then M + N c= {} by SUBSET_1:7;
hence M + N = {} ; :: thesis: verum