let p, q be FinSequence; :: thesis: ( p c< q iff ( len p < len q & ( for i being Nat st i in dom p holds
p . i = q . i ) ) )

hereby :: thesis: ( len p < len q & ( for i being Nat st i in dom p holds
p . i = q . i ) implies p c< q )

assume Z0: p c< q ; :: thesis: ( len p < len q & ( for i being Nat st i in dom p holds
p . i = q . i ) )
hence len p < len q by TREES_1:6; :: thesis: for i being Nat st i in dom p holds
p . i = q . i
p c= q by Z0, XBOOLE_0:def 8;
hence for i being Nat st i in dom p holds
p . i = q . i by FOMODEL0:51; :: thesis: verum

end;

assume Z2: len p < len q ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum