let a, b be FinSequence; :: 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 A2: a ^ b = a ; :: thesis: b = {}

len (a ^ b) = (len a) + (len b) by FINSEQ_1:22;
hence b = {} by A2; :: thesis: verum

end;

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

len (b ^ a) = (len b) + (len a) by FINSEQ_1:22;
hence b = {} by A3; :: thesis: verum

end;

end;