let p, q be FinSequence; ( p c< q iff ( len p < len q & ( for i being Nat st i in dom p holds
p . i = q . i ) ) )
hereby ( len p < len q & ( for i being Nat st i in dom p holds
p . i = q . i ) implies p c< q )
end;
assume Z2:
len p < len q
; ( ex i being Nat st
( i in dom p & not p . i = q . i ) or p c< q )
then
dom p c< dom q
by FINSEQ_3:118;
then A1:
dom p c= dom q
by XBOOLE_0:def 8;
assume
for i being Nat st i in dom p holds
p . i = q . i
; p c< q
then
for i being set st i in dom p holds
( i in dom q & p . i = q . i )
by A1;
hence
p c< q
by Z2, XBOOLE_0:def 8, FOMODEL0:51; verum