let i be Nat; :: thesis: for p, q being FinSequence st i in dom p holds
i in dom (p ^ q)
let p, q be FinSequence; :: thesis: ( i in dom p implies i in dom (p ^ q) )
assume i in dom p ; :: thesis: i in dom (p ^ q)
then ( i in dom p & dom p c= dom (p ^ q) ) by FINSEQ_1:39;
hence i in dom (p ^ q) ; :: thesis: verum