let f, g be FinSequence; :: thesis: ( dom f c= dom g or dom g c= dom f )
consider n being Nat such that
A1: dom f = Seg n by FINSEQ_1:def 2;
consider m being Nat such that
A2: dom g = Seg m by FINSEQ_1:def 2;
( m <= n or n <= m ) ;
hence ( dom f c= dom g or dom g c= dom f ) by A1, A2, FINSEQ_1:5; :: thesis: verum