let i be natural Number ; :: 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) )
A1: dom p c= dom (p ^ q) by FINSEQ_1:26;
assume i in dom p ; :: thesis: i in dom (p ^ q)
hence i in dom (p ^ q) by A1; :: thesis: verum