let p, q be FinSequence; :: thesis: for A being set holds p " A c= (p ^ q) " A
let A be set ; :: thesis: p " A c= (p ^ q) " A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in p " A or x in (p ^ q) " A )
A1: dom p c= dom (p ^ q) by FINSEQ_1:26;
assume A2: x in p " A ; :: thesis: x in (p ^ q) " A
then A3: x in dom p by FUNCT_1:def 7;
then reconsider k = x as Element of NAT ;
A4: p . k in A by A2, FUNCT_1:def 7;
p . k = (p ^ q) . k by A3, FINSEQ_1:def 7;
hence x in (p ^ q) " A by A3, A1, A4, FUNCT_1:def 7; :: thesis: verum