let a be Nat; :: thesis: for fs being FinSequence holds dom (Del (fs,a)) c= dom fs
let fs be FinSequence; :: thesis: dom (Del (fs,a)) c= dom fs
now :: thesis: ( a in dom fs implies dom (Del (fs,a)) c= dom fs )
assume A1: a in dom fs ; :: thesis: dom (Del (fs,a)) c= dom fs
dom fs = Seg (len fs) by FINSEQ_1:def 3
.= Seg ((len (Del (fs,a))) + 1) by A1, Def1
.= (Seg (len (Del (fs,a)))) \/ {((len (Del (fs,a))) + 1)} by FINSEQ_1:9
.= (dom (Del (fs,a))) \/ {((len (Del (fs,a))) + 1)} by FINSEQ_1:def 3 ;
hence dom (Del (fs,a)) c= dom fs by XBOOLE_1:7; :: thesis: verum
end;
hence dom (Del (fs,a)) c= dom fs by Def1; :: thesis: verum