defpred S₁[ PNPair] means ( rng ($1 `1) = untn (rng (P `1)) & rng ($1 `2) = untn (rng (P `2)) );
set s = (untn (rng (P `1))) \/ (untn (rng (P `2)));
consider f being FinSequence such that
A1: rng f = untn (rng (P `1)) and
A2: f is one-to-one by FINSEQ_4:58;
reconsider f = f as one-to-one FinSequence of LTLB_WFF by A1, A2, FINSEQ_1:def 4;
consider g being FinSequence such that
A3: rng g = untn (rng (P `2)) and
A4: g is one-to-one by FINSEQ_4:58;
reconsider g = g as one-to-one FinSequence of LTLB_WFF by A3, A4, FINSEQ_1:def 4;
A5: rng ([f,g] `1) = untn (rng (P `1)) by A1;
A6: { A where A is PNPair : S₁[A] } c= [:(((untn (rng (P `1))) \/ (untn (rng (P `2)))) **),(((untn (rng (P `1))) \/ (untn (rng (P `2)))) **):]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is PNPair : S₁[A] } or x in [:(((untn (rng (P `1))) \/ (untn (rng (P `2)))) **),(((untn (rng (P `1))) \/ (untn (rng (P `2)))) **):] )
assume x in { A where A is PNPair : S₁[A] } ; :: thesis: x in [:(((untn (rng (P `1))) \/ (untn (rng (P `2)))) **),(((untn (rng (P `1))) \/ (untn (rng (P `2)))) **):]
then consider Q being PNPair such that
A7: x = Q and
A8: rng (Q `1) = untn (rng (P `1)) and
A9: rng (Q `2) = untn (rng (P `2)) ;
consider y, z being object such that
A10: ( y in LTLB_WFF ** & z in LTLB_WFF ** ) and
A11: Q = [y,z] by ZFMISC_1:def 2;
reconsider y = y, z = z as one-to-one FinSequence of LTLB_WFF by A10, LTLAXIO3:def 2;
rng (Q `1) c= (untn (rng (P `1))) \/ (untn (rng (P `2))) by A8, XBOOLE_1:7;
then A12: rng y c= (untn (rng (P `1))) \/ (untn (rng (P `2))) by A11;
rng (Q `2) c= (untn (rng (P `1))) \/ (untn (rng (P `2))) by A9, XBOOLE_1:7;
then A13: rng z c= (untn (rng (P `1))) \/ (untn (rng (P `2))) by A11;
reconsider y = y as one-to-one FinSequence of (untn (rng (P `1))) \/ (untn (rng (P `2))) by A12, FINSEQ_1:def 4;
reconsider z = z as one-to-one FinSequence of (untn (rng (P `1))) \/ (untn (rng (P `2))) by A13, FINSEQ_1:def 4;
( y in ((untn (rng (P `1))) \/ (untn (rng (P `2)))) ** & z in ((untn (rng (P `1))) \/ (untn (rng (P `2)))) ** ) by LTLAXIO3:def 2;
hence x in [:(((untn (rng (P `1))) \/ (untn (rng (P `2)))) **),(((untn (rng (P `1))) \/ (untn (rng (P `2)))) **):] by ZFMISC_1:def 2, A11, A7; :: thesis: verum

end;

rng ([f,g] `2) = untn (rng (P `2)) by A3;
then A14: [f,g] in { A where A is PNPair : S₁[A] } by A5;
{ A where A is PNPair : S₁[A] } c= [:(LTLB_WFF **),(LTLB_WFF **):] from FRAENKEL:sch 10();
hence { Q where Q is PNPair : ( rng (Q `1) = untn (rng (P `1)) & rng (Q `2) = untn (rng (P `2)) ) } is non empty finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] by A14, A6; :: thesis: verum