let p, q be FinSequence; :: thesis: for x being object st x in dom p holds
x in dom (p ^ q)
let x be object ; :: thesis: ( x in dom p implies x in dom (p ^ q) )
dom p c= dom (p ^ q) by FINSEQ_1:26;
hence ( x in dom p implies x in dom (p ^ q) ) ; :: thesis: verum