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

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