let P1, S1, S2 be FinSequence-membered set ; :: thesis: P1 ^ (S1 \/ S2) = (P1 ^ S1) \/ (P1 ^ S2)
thus P1 ^ (S1 \/ S2) c= (P1 ^ S1) \/ (P1 ^ S2) :: according to XBOOLE_0:def 10 :: thesis: (P1 ^ S1) \/ (P1 ^ S2) c= P1 ^ (S1 \/ S2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 ^ (S1 \/ S2) or x in (P1 ^ S1) \/ (P1 ^ S2) )
assume A1: x in P1 ^ (S1 \/ S2) ; :: thesis: x in (P1 ^ S1) \/ (P1 ^ S2)
consider p, q being FinSequence such that
A2: ( x = p ^ q & p in P1 & q in S1 \/ S2 ) by A1, POLNOT_1:def 2;
( q in S1 or q in S2 ) by A2, XBOOLE_0:def 3;
then ( x in P1 ^ S1 or x in P1 ^ S2 ) by A2, POLNOT_1:def 2;
hence x in (P1 ^ S1) \/ (P1 ^ S2) by XBOOLE_0:def 3; :: thesis: verum

end;

A3: P1 ^ S1 c= P1 ^ (S1 \/ S2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 ^ S1 or x in P1 ^ (S1 \/ S2) )
assume A4: x in P1 ^ S1 ; :: thesis: x in P1 ^ (S1 \/ S2)
consider p, q being FinSequence such that
A5: ( x = p ^ q & p in P1 & q in S1 ) by A4, POLNOT_1:def 2;
q in S1 \/ S2 by A5, XBOOLE_0:def 3;
hence x in P1 ^ (S1 \/ S2) by A5, POLNOT_1:def 2; :: thesis: verum

end;

P1 ^ S2 c= P1 ^ (S1 \/ S2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 ^ S2 or x in P1 ^ (S1 \/ S2) )
assume A6: x in P1 ^ S2 ; :: thesis: x in P1 ^ (S1 \/ S2)
consider p, q being FinSequence such that
A7: ( x = p ^ q & p in P1 & q in S2 ) by A6, POLNOT_1:def 2;
q in S1 \/ S2 by A7, XBOOLE_0:def 3;
hence x in P1 ^ (S1 \/ S2) by A7, POLNOT_1:def 2; :: thesis: verum

end;

hence (P1 ^ S1) \/ (P1 ^ S2) c= P1 ^ (S1 \/ S2) by A3, XBOOLE_1:8; :: thesis: verum