let P1, P2, Q1, Q2 be FinSequence-membered set ; :: thesis: ( P1 c= P2 & Q1 c= Q2 implies P1 ^ Q1 c= P2 ^ Q2 )
assume A1: ( P1 c= P2 & Q1 c= Q2 ) ; :: thesis: P1 ^ Q1 c= P2 ^ Q2
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in P1 ^ Q1 or a in P2 ^ Q2 )
assume a in P1 ^ Q1 ; :: thesis: a in P2 ^ Q2
then consider p, q being FinSequence such that
A3: ( a = p ^ q & p in P1 & q in Q1 ) by Def2;
thus a in P2 ^ Q2 by A1, A3, Def2; :: thesis: verum