let F, G be FinSequence-yielding FinSequence; :: thesis: for P, S being FinSequence-membered set st P c= doms F & S c= doms G holds
P ^ S c= doms (F ^ G)
let P, S be FinSequence-membered set ; :: thesis: ( P c= doms F & S c= doms G implies P ^ S c= doms (F ^ G) )
assume A1: ( P c= doms F & S c= doms G ) ; :: thesis: P ^ S c= doms (F ^ G)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P ^ S or x in doms (F ^ G) )
assume A2: x in P ^ S ; :: thesis: x in doms (F ^ G)
ex p, s being FinSequence st
( x = p ^ s & p in P & s in S ) by A2, POLNOT_1:def 2;
hence x in doms (F ^ G) by A1, Th48; :: thesis: verum