let E be set ; :: thesis: for a, b being Element of E ^omega st ( a ^ b = a or b ^ a = a ) holds
b = {}
let a, b be Element of E ^omega ; :: thesis: ( ( a ^ b = a or b ^ a = a ) implies b = {} )
assume A1: ( a ^ b = a or b ^ a = a ) ; :: thesis: b = {}

per cases ( a ^ b = a or b ^ a = a ) by A1;

suppose a ^ b = a ; :: thesis: b = {}

then ( len (a ^ b) = (len a) + (len b) & len (a ^ b) = len a ) by AFINSQ_1:20;
hence b = {} by AFINSQ_1:18; :: thesis: verum

end;

suppose b ^ a = a ; :: thesis: b = {}

then ( len (b ^ a) = (len b) + (len a) & len (b ^ a) = len a ) by AFINSQ_1:20;
hence b = {} by AFINSQ_1:18; :: thesis: verum

end;

end;