let x be set ; :: thesis: for p, q being FinSequence holds
( not p ^ q = <*x*> or ( p = <*x*> & q = {} ) or ( p = {} & q = <*x*> ) )
let p, q be FinSequence; :: thesis: ( not p ^ q = <*x*> or ( p = <*x*> & q = {} ) or ( p = {} & q = <*x*> ) )
assume A1: p ^ q = <*x*> ; :: thesis: ( ( p = <*x*> & q = {} ) or ( p = {} & q = <*x*> ) )
A2: 1 = len (p ^ q) by A1, Th57
.= (len p) + (len q) by Th35 ;

A3: now

assume A4: len p = 0 ; :: thesis: ( p = {} & q = <*x*> )
thus A5: p = {} by A4; :: thesis: q = <*x*>
thus q = <*x*> by A1, A5, Th47; :: thesis: verum

end;

A6: now

assume A7: len p <> 0 ; :: thesis: ( q = {} & p = <*x*> )
A8: 0 + 1 <= len p by A7, NAT_1:13;
A9: len p <= 1 by A2, NAT_1:11;
A10: len p = 1 by A8, A9, XXREAL_0:1;
thus A11: q = {} by A2, A10; :: thesis: p = <*x*>
thus p = <*x*> by A1, A11, Th47; :: thesis: verum

end;

thus ( ( p = <*x*> & q = {} ) or ( p = {} & q = <*x*> ) ) by A3, A6; :: thesis: verum