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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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