let p, q, r, s be FinSequence; :: thesis: ( p ^ q = r ^ s implies ex t being FinSequence st
( p ^ t = r or p = r ^ t ) )
assume A1: p ^ q = r ^ s ; :: thesis: ex t being FinSequence st
( p ^ t = r or p = r ^ t )

per cases ( len p <= len r or len p > len r ) ;

suppose len p <= len r ; :: thesis: ex t being FinSequence st
( p ^ t = r or p = r ^ t )

then consider u being FinSequence such that
A2: p ^ u = r by A1, FINSEQ_1:47;
take u ; :: thesis: ( p ^ u = r or p = r ^ u )
thus ( p ^ u = r or p = r ^ u ) by A2; :: thesis: verum

end;

suppose len p > len r ; :: thesis: ex t being FinSequence st
( p ^ t = r or p = r ^ t )

then consider u being FinSequence such that
A3: r ^ u = p by A1, FINSEQ_1:47;
take u ; :: thesis: ( p ^ u = r or p = r ^ u )
thus ( p ^ u = r or p = r ^ u ) by A3; :: thesis: verum

end;

end;