let x be object ; :: 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*> ) )
then A2: 1 = len (p ^ q) by Th40
.= (len p) + (len q) by Th22 ;

A3: now :: thesis: ( len p = 0 implies ( p = {} & q = <*x*> ) )

assume len p = 0 ; :: thesis: ( p = {} & q = <*x*> )
hence p = {} ; :: thesis: q = <*x*>
hence q = <*x*> by A1, Th34; :: thesis: verum

end;

now :: thesis: ( len p <> 0 implies ( q = {} & p = <*x*> ) )

assume len p <> 0 ; :: thesis: ( q = {} & p = <*x*> )
then A4: 0 + 1 <= len p by NAT_1:13;
len p <= 1 by A2, NAT_1:11;
then len p = 1 by A4, XXREAL_0:1;
hence q = {} by A2; :: thesis: p = <*x*>
hence p = <*x*> by A1, Th34; :: thesis: verum

end;

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