let P be consistent PNPair; :: thesis: ex P1 being consistent PNPair st
( rng (P `1) c= rng (P1 `1) & rng (P `2) c= rng (P1 `2) & tau (rng P) = rng P1 )
set tfp = (tau (rng P)) \ (rng P);
consider t being FinSequence such that
A1: rng t = (tau (rng P)) \ (rng P) and
A2: t is one-to-one by FINSEQ_4:58;
reconsider t = t as one-to-one FinSequence of LTLB_WFF by FINSEQ_1:def 4, A1, A2;
defpred S1[ Nat, Element of [:(LTLB_WFF **),(LTLB_WFF **):], Element of [:(LTLB_WFF **),(LTLB_WFF **):]] means ( $2 is consistent implies ( ( [(($2 `1) ^^ <*(t /. $1)*>),($2 `2)] is consistent implies $3 = [(($2 `1) ^^ <*(t /. $1)*>),($2 `2)] ) & ( not [(($2 `1) ^^ <*(t /. $1)*>),($2 `2)] is consistent implies $3 = [($2 `1),(($2 `2) ^^ <*(t /. $1)*>)] ) ) );
A3: now :: thesis: for n being Nat st 1 <= n & n <= ((len t) + 1) - 1 holds
for x being Element of [:(LTLB_WFF **),(LTLB_WFF **):] ex y being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st S1[n,x,y]
let n be Nat; :: thesis: ( 1 <= n & n <= ((len t) + 1) - 1 implies for x being Element of [:(LTLB_WFF **),(LTLB_WFF **):] ex y being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st S1[n,x,y] )
assume that
1 <= n and
n <= ((len t) + 1) - 1 ; :: thesis: for x being Element of [:(LTLB_WFF **),(LTLB_WFF **):] ex y being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st S1[n,x,y]
let x be Element of [:(LTLB_WFF **),(LTLB_WFF **):]; :: thesis: ex y being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st S1[n,x,y]
( [((x `1) ^^ <*(t /. n)*>),(x `2)] is consistent or not [((x `1) ^^ <*(t /. n)*>),(x `2)] is consistent ) ;
hence ex y being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st S1[n,x,y] ; :: thesis: verum
end;
consider pn being FinSequence of [:(LTLB_WFF **),(LTLB_WFF **):] such that
A4: ( len pn = (len t) + 1 & ( pn /. 1 = P or (len t) + 1 = 0 ) & ( for n being Nat st 1 <= n & n <= ((len t) + 1) - 1 holds
S1[n,pn /. n,pn /. (n + 1)] ) ) from RECDEF_1:sch 18(A3);
 defpred S2[ Nat] means ( $1 <= len pn implies ( ( $1 <= len t implies rng (pn /. $1) misses (rng <*(t /. $1)*>) \/ (rng (t /^ $1)) ) & pn /. $1 is consistent & rng P c= rng (pn /. $1) ) );
A5: for k being non zero Nat st S2[k] holds
S2[k + 1]
proof
let k be non zero Nat; :: thesis: ( S2[k] implies S2[k + 1] )
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
A6: 1 <= k by NAT_1:25;
A7: k + 1 > k by NAT_1:13;
assume A8: S2[k] ; :: thesis: S2[k + 1]
A9: 1 <= k + 1 by NAT_1:25;
thus S2[k + 1] :: thesis: verum
proof
t /. k1 in {(t /. k1)} by TARSKI:def 1;
then A10: t /. k1 in rng <*(t /. k1)*> by FINSEQ_1:39;
assume A11: k + 1 <= len pn ; :: thesis: ( ( k + 1 <= len t implies rng (pn /. (k + 1)) misses (rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))) ) & pn /. (k + 1) is consistent & rng P c= rng (pn /. (k + 1)) )
then reconsider P1 = pn /. k1 as consistent PNPair by NAT_1:13, A8;
set pp = [((P1 `1) ^^ <*(t /. k1)*>),(P1 `2)];
set pp2 = [(P1 `1),((P1 `2) ^^ <*(t /. k1)*>)];
A12: rng P1 misses rng (t /^ k1) by XBOOLE_1:7, XBOOLE_1:63, A8, A4, A11, XREAL_1:6, NAT_1:13;
rng P1 misses rng <*(t /. k1)*> by XBOOLE_1:63, XBOOLE_1:7, A8, A4, A11, XREAL_1:6, NAT_1:13;
then A13: rng (P1 `2) misses rng <*(t /. k1)*> by XBOOLE_1:7, XBOOLE_1:63;
A14: rng P1 misses rng <*(t /. k1)*> by XBOOLE_1:7, XBOOLE_1:63, A8, A4, A11, XREAL_1:6, NAT_1:13;
then A15: rng (P1 `1) misses rng <*(t /. k1)*> by XBOOLE_1:7, XBOOLE_1:63;
(rng P1) /\ (rng <*(t /. k1)*>) = {} by A14;
then A16: not t /. k1 in rng P1 by A10, XBOOLE_0:def 4;
A17: (k + 1) + (- 1) <= ((len t) + 1) + (- 1) by A4, A11, XREAL_1:6;
then A18: k in dom t by FINSEQ_3:25, A6;
A19: S1[k1,P1,pn /. (k1 + 1)] by A4, A6, A17;
set r1 = [((P1 `1) ^^ <*(t /. k1)*>),([((P1 `1) ^^ <*(t /. k1)*>),(P1 `2)] `2)];
set r2 = [([(P1 `1),((P1 `2) ^^ <*(t /. k1)*>)] `1),((P1 `2) ^^ <*(t /. k1)*>)];
per cases ( [((P1 `1) ^^ <*(t /. k1)*>),(P1 `2)] is consistent or not [((P1 `1) ^^ <*(t /. k1)*>),(P1 `2)] is consistent ) ;
suppose A20: [((P1 `1) ^^ <*(t /. k1)*>),(P1 `2)] is consistent ; :: thesis: ( ( k + 1 <= len t implies rng (pn /. (k + 1)) misses (rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))) ) & pn /. (k + 1) is consistent & rng P c= rng (pn /. (k + 1)) )
then A21: rng (pn /. (k + 1)) = (rng ([((P1 `1) ^^ <*(t /. k1)*>),([((P1 `1) ^^ <*(t /. k1)*>),(P1 `2)] `2)] `1)) \/ (rng ([((P1 `1) ^^ <*(t /. k1)*>),([((P1 `1) ^^ <*(t /. k1)*>),(P1 `2)] `2)] `2)) by A19
.= (rng ((P1 `1) ^ <*(t /. k1)*>)) \/ (rng (P1 `2)) by Def3, A15
.= ((rng (P1 `1)) \/ (rng <*(t /. k1)*>)) \/ (rng (P1 `2)) by FINSEQ_1:31
.= (rng P1) \/ (rng <*(t /. k1)*>) by XBOOLE_1:4 ;
thus ( k + 1 <= len t implies rng (pn /. (k + 1)) misses (rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))) ) :: thesis: ( pn /. (k + 1) is consistent & rng P c= rng (pn /. (k + 1)) )
proof
assume A22: k + 1 <= len t ; :: thesis: rng (pn /. (k + 1)) misses (rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1)))
then <*(t . (k + 1))*> ^ (t /^ (k + 1)) = t /^ k by Th1;
then (rng <*(t . (k + 1))*>) \/ (rng (t /^ (k + 1))) = rng (t /^ k) by FINSEQ_1:31;
then A23: rng (t /^ (k + 1)) c= rng (t /^ k) by XBOOLE_1:7;
k + 1 in dom t by FINSEQ_3:25, A22, A9;
then {(t /. (k + 1))} c= rng (t /^ k) by FINSEQ_6:58, A7, ZFMISC_1:31;
then rng <*(t /. (k + 1))*> c= rng (t /^ k) by FINSEQ_1:39;
then A24: (rng (t /^ (k + 1))) \/ (rng <*(t /. (k + 1))*>) c= (rng (t /^ k)) \/ (rng (t /^ k)) by XBOOLE_1:13, A23;
k1 in Seg k1 by A6;
then t . k1 in rng (t | (Seg k)) by FUNCT_1:50, A18;
then t /. k1 in rng (t | k) by PARTFUN1:def 6, A18;
then {(t /. k1)} c= rng (t | k) by ZFMISC_1:31;
then rng <*(t /. k1)*> c= rng (t | k) by FINSEQ_1:39;
then A25: rng <*(t /. k1)*> misses (rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))) by FINSEQ_5:34, XBOOLE_1:64, A24;
(rng (pn /. (k + 1))) /\ ((rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1)))) = ((rng P1) /\ ((rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))))) \/ ((rng <*(t /. k1)*>) /\ ((rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))))) by XBOOLE_1:23, A21
.= {} \/ ((rng <*(t /. k1)*>) /\ ((rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))))) by A24, XBOOLE_1:63, A12, XBOOLE_0:def 7
.= {} by A25 ;
hence rng (pn /. (k + 1)) misses (rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))) ; :: thesis: verum
end;
thus pn /. (k + 1) is consistent by A4, A6, A17, A20; :: thesis: rng P c= rng (pn /. (k + 1))
rng (pn /. k) c= rng (pn /. (k + 1)) by XBOOLE_1:7, A21;
hence rng P c= rng (pn /. (k + 1)) by A8, A11, NAT_1:13; :: thesis: verum
end;
suppose not [((P1 `1) ^^ <*(t /. k1)*>),(P1 `2)] is consistent ; :: thesis: ( ( k + 1 <= len t implies rng (pn /. (k + 1)) misses (rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))) ) & pn /. (k + 1) is consistent & rng P c= rng (pn /. (k + 1)) )
then A26: rng (pn /. (k + 1)) = (rng ([([(P1 `1),((P1 `2) ^^ <*(t /. k1)*>)] `1),((P1 `2) ^^ <*(t /. k1)*>)] `1)) \/ (rng ([([(P1 `1),((P1 `2) ^^ <*(t /. k1)*>)] `1),((P1 `2) ^^ <*(t /. k1)*>)] `2)) by A19
.= (rng (P1 `1)) \/ (rng ((P1 `2) ^ <*(t /. k1)*>)) by Def3, A13
.= (rng (P1 `1)) \/ ((rng (P1 `2)) \/ (rng <*(t /. k1)*>)) by FINSEQ_1:31
.= (rng P1) \/ (rng <*(t /. k1)*>) by XBOOLE_1:4 ;
thus ( k + 1 <= len t implies rng (pn /. (k + 1)) misses (rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))) ) :: thesis: ( pn /. (k + 1) is consistent & rng P c= rng (pn /. (k + 1)) )
proof
assume A27: k + 1 <= len t ; :: thesis: rng (pn /. (k + 1)) misses (rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1)))
then <*(t . (k + 1))*> ^ (t /^ (k + 1)) = t /^ k by Th1;
then (rng <*(t . (k + 1))*>) \/ (rng (t /^ (k + 1))) = rng (t /^ k) by FINSEQ_1:31;
then A28: rng (t /^ (k + 1)) c= rng (t /^ k) by XBOOLE_1:7;
k + 1 in dom t by FINSEQ_3:25, A27, A9;
then {(t /. (k + 1))} c= rng (t /^ k) by FINSEQ_6:58, A7, ZFMISC_1:31;
then rng <*(t /. (k + 1))*> c= rng (t /^ k) by FINSEQ_1:39;
then A29: (rng (t /^ (k + 1))) \/ (rng <*(t /. (k + 1))*>) c= (rng (t /^ k)) \/ (rng (t /^ k)) by XBOOLE_1:13, A28;
k1 in Seg k1 by A6;
then t . k1 in rng (t | (Seg k)) by FUNCT_1:50, A18;
then t /. k1 in rng (t | k) by PARTFUN1:def 6, A18;
then {(t /. k1)} c= rng (t | k) by ZFMISC_1:31;
then rng <*(t /. k1)*> c= rng (t | k) by FINSEQ_1:39;
then A30: rng <*(t /. k1)*> misses (rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))) by FINSEQ_5:34, XBOOLE_1:64, A29;
(rng (pn /. (k + 1))) /\ ((rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1)))) = ((rng P1) /\ ((rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))))) \/ ((rng <*(t /. k1)*>) /\ ((rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))))) by XBOOLE_1:23, A26
.= {} \/ ((rng <*(t /. k1)*>) /\ ((rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))))) by A29, XBOOLE_1:63, A12, XBOOLE_0:def 7
.= {} by A30 ;
hence rng (pn /. (k + 1)) misses (rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))) ; :: thesis: verum
end;
thus pn /. (k + 1) is consistent by A19, Th31, A16; :: thesis: rng P c= rng (pn /. (k + 1))
rng (pn /. k) c= rng (pn /. (k + 1)) by XBOOLE_1:7, A26;
hence rng P c= rng (pn /. (k + 1)) by A8, A11, NAT_1:13; :: thesis: verum
end;
end;
end;
end;
reconsider lpn = len pn as non zero Nat by A4;
A31: S2[1]
proof
assume 1 <= len pn ; :: thesis: ( ( 1 <= len t implies rng (pn /. 1) misses (rng <*(t /. 1)*>) \/ (rng (t /^ 1)) ) & pn /. 1 is consistent & rng P c= rng (pn /. 1) )
thus ( 1 <= len t implies rng (pn /. 1) misses (rng <*(t /. 1)*>) \/ (rng (t /^ 1)) ) :: thesis: ( pn /. 1 is consistent & rng P c= rng (pn /. 1) )
proof
assume 1 <= len t ; :: thesis: rng (pn /. 1) misses (rng <*(t /. 1)*>) \/ (rng (t /^ 1))
then A32: t <> {} ;
(rng <*(t /. 1)*>) \/ (rng (t /^ 1)) = rng (<*(t /. 1)*> ^ (t /^ 1)) by FINSEQ_1:31
.= rng (t :- (t /. 1)) by FINSEQ_6:43, A32
.= rng t by FINSEQ_6:44, A32 ;
hence rng (pn /. 1) misses (rng <*(t /. 1)*>) \/ (rng (t /^ 1)) by A4, XBOOLE_1:79, A1; :: thesis: verum
end;
thus pn /. 1 is consistent by A4; :: thesis: rng P c= rng (pn /. 1)
thus rng P c= rng (pn /. 1) by A4; :: thesis: verum
end;
A33: for k being non zero Nat holds S2[k] from NAT_1:sch 10(A31, A5);
 then pn /. lpn is consistent ;
then reconsider P2 = pn /. (len pn) as consistent PNPair ;
set i2 = (len pn) -' 1;
set P3 = pn /. lpn;
A34: (len pn) -' ((len pn) -' 1) = (len pn) -' ((len pn) - 1) by A4, XREAL_0:def 2
.= (len pn) - ((len pn) - 1) by XREAL_0:def 2
.= 1 ;
defpred S3[ Nat] means ( $1 < len pn implies ( rng ((pn /. ((len pn) -' $1)) `1) c= rng (P2 `1) & rng ((pn /. ((len pn) -' $1)) `2) c= rng (P2 `2) ) );
A35: now :: thesis: for n being Element of NAT st 1 <= n & n <= len t holds
( rng ((pn /. n) `1) misses rng <*(t /. n)*> & rng ((pn /. n) `2) misses rng <*(t /. n)*> )
let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len t implies ( rng ((pn /. n) `1) misses rng <*(t /. n)*> & rng ((pn /. n) `2) misses rng <*(t /. n)*> ) )
assume that
A36: 1 <= n and
A37: n <= len t ; :: thesis: ( rng ((pn /. n) `1) misses rng <*(t /. n)*> & rng ((pn /. n) `2) misses rng <*(t /. n)*> )
n <= len pn by A37, NAT_1:13, A4;
then rng (pn /. n) misses (rng <*(t /. n)*>) \/ (rng (t /^ n)) by A33, A36, A37;
then A38: rng (pn /. n) misses rng <*(t /. n)*> by XBOOLE_1:7, XBOOLE_1:63;
hence rng ((pn /. n) `1) misses rng <*(t /. n)*> by XBOOLE_1:7, XBOOLE_1:63; :: thesis: rng ((pn /. n) `2) misses rng <*(t /. n)*>
thus rng ((pn /. n) `2) misses rng <*(t /. n)*> by XBOOLE_1:7, XBOOLE_1:63, A38; :: thesis: verum
end;
A39: now :: thesis: for n being Nat st S3[n] holds
S3[n + 1]
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
set k = (len pn) -' (n + 1);
assume A40: S3[n] ; :: thesis: S3[n + 1]
thus S3[n + 1] :: thesis: verum
proof
assume A41: n + 1 < len pn ; :: thesis: ( rng ((pn /. ((len pn) -' (n + 1))) `1) c= rng (P2 `1) & rng ((pn /. ((len pn) -' (n + 1))) `2) c= rng (P2 `2) )
then A42: (n + 1) + (- 1) < len pn by XREAL_1:36;
then A43: n + (- n) < (len pn) + (- n) by XREAL_1:8;
A44: (n + 1) + (- (n + 1)) < (len pn) + (- (n + 1)) by A41, XREAL_1:8;
then A45: (len pn) -' (n + 1) = (len pn) - (n + 1) by XREAL_0:def 2
.= (len t) - n by A4 ;
A46: (len pn) - (n + 1) > 0 by A44;
then (len pn) -' (n + 1) > 0 by XREAL_0:def 2;
then A47: 1 <= (len pn) -' (n + 1) by NAT_1:25;
reconsider k = (len pn) -' (n + 1) as non zero Element of NAT by XREAL_0:def 2, A46;
set P1 = pn /. k;
A48: len t >= (len t) + (- n) by XREAL_1:32;
then A49: rng ((pn /. k) `2) misses rng <*(t /. k)*> by A35, A47, A45;
A50: rng ((pn /. k) `1) misses rng <*(t /. k)*> by A35, A47, A48, A45;
A51: k + 1 = ((len pn) - (n + 1)) + 1 by XREAL_0:def 2
.= (len pn) - n
.= (len pn) -' n by XREAL_0:def 2, A43 ;
k < len pn by A4, NAT_1:13, A48, A45;
then A52: pn /. k is consistent PNPair by A33;
per cases ( [(((pn /. k) `1) ^^ <*(t /. k)*>),((pn /. k) `2)] is consistent or not [(((pn /. k) `1) ^^ <*(t /. k)*>),((pn /. k) `2)] is consistent ) ;
suppose [(((pn /. k) `1) ^^ <*(t /. k)*>),((pn /. k) `2)] is consistent ; :: thesis: ( rng ((pn /. ((len pn) -' (n + 1))) `1) c= rng (P2 `1) & rng ((pn /. ((len pn) -' (n + 1))) `2) c= rng (P2 `2) )
then A53: pn /. (k + 1) = [(((pn /. k) `1) ^^ <*(t /. k)*>),((pn /. k) `2)] by A47, A48, A45, A4, A52;
then rng (((pn /. k) `1) ^^ <*(t /. k)*>) c= rng (P2 `1) by A40, A42, A51;
then rng (((pn /. k) `1) ^ <*(t /. k)*>) c= rng (P2 `1) by A50, Def3;
then A54: (rng ((pn /. k) `1)) \/ (rng <*(t /. k)*>) c= rng (P2 `1) by FINSEQ_1:31;
rng ((pn /. k) `1) c= (rng ((pn /. k) `1)) \/ (rng <*(t /. k)*>) by XBOOLE_1:7;
hence ( rng ((pn /. ((len pn) -' (n + 1))) `1) c= rng (P2 `1) & rng ((pn /. ((len pn) -' (n + 1))) `2) c= rng (P2 `2) ) by A40, A42, A51, A53, A54; :: thesis: verum
end;
suppose not [(((pn /. k) `1) ^^ <*(t /. k)*>),((pn /. k) `2)] is consistent ; :: thesis: ( rng ((pn /. ((len pn) -' (n + 1))) `1) c= rng (P2 `1) & rng ((pn /. ((len pn) -' (n + 1))) `2) c= rng (P2 `2) )
then A55: pn /. (k + 1) = [((pn /. k) `1),(((pn /. k) `2) ^^ <*(t /. k)*>)] by A47, A48, A45, A4, A52;
then rng (((pn /. k) `2) ^^ <*(t /. k)*>) c= rng (P2 `2) by A40, A42, A51;
then rng (((pn /. k) `2) ^ <*(t /. k)*>) c= rng (P2 `2) by A49, Def3;
then A56: (rng ((pn /. k) `2)) \/ (rng <*(t /. k)*>) c= rng (P2 `2) by FINSEQ_1:31;
rng ((pn /. k) `2) c= (rng ((pn /. k) `2)) \/ (rng <*(t /. k)*>) by XBOOLE_1:7;
hence ( rng ((pn /. ((len pn) -' (n + 1))) `1) c= rng (P2 `1) & rng ((pn /. ((len pn) -' (n + 1))) `2) c= rng (P2 `2) ) by A56, A55, A40, A42, A51; :: thesis: verum
end;
end;
end;
end;
A57: S3[ 0 ]
proof
assume 0 < len pn ; :: thesis: ( rng ((pn /. ((len pn) -' 0)) `1) c= rng (P2 `1) & rng ((pn /. ((len pn) -' 0)) `2) c= rng (P2 `2) )
then (len pn) - 0 > 0 ;
hence ( rng ((pn /. ((len pn) -' 0)) `1) c= rng (P2 `1) & rng ((pn /. ((len pn) -' 0)) `2) c= rng (P2 `2) ) by XREAL_0:def 2; :: thesis: verum
end;
A58: for n being Nat holds S3[n] from NAT_1:sch 2(A57, A39);
 then A59: ( (len pn) + (- 1) < len pn & S3[(len pn) -' 1] ) by XREAL_1:30;
A60: tau (rng P) c= rng P2
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tau (rng P) or x in rng P2 )
assume x in tau (rng P) ; :: thesis: x in rng P2
then A61: x in ((tau (rng P)) \ (rng P)) \/ (rng P) by XBOOLE_1:45, Th16;
per cases ( x in (tau (rng P)) \ (rng P) or x in rng P ) by A61, XBOOLE_0:def 3;
suppose x in (tau (rng P)) \ (rng P) ; :: thesis: x in rng P2
then consider i being Nat such that
A62: i in dom t and
A63: t . i = x by A1, FINSEQ_2:10;
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
set P5 = pn /. i1;
A64: i <= ((len t) + 1) - 1 by FINSEQ_3:25, A62;
then A65: i < len pn by A4, NAT_1:13;
reconsider ii = (len pn) -' (i + 1) as Element of NAT ;
set P3 = pn /. ((len pn) -' ii);
(- 1) * (i + 1) < (- 1) * 0 by XREAL_1:69;
then A66: (len pn) + (- (i + 1)) < len pn by XREAL_1:30;
A67: 1 <= i by FINSEQ_3:25, A62;
then A68: S1[i1,pn /. i1,pn /. (i1 + 1)] by A64, A4;
A69: i <= len t by FINSEQ_3:25, A62;
then A70: rng ((pn /. i1) `1) misses rng <*(t /. i)*> by A35, A67;
A71: rng ((pn /. i1) `2) misses rng <*(t /. i)*> by A35, A67, A69;
i + 1 <= len pn by XREAL_1:6, A69, A4;
then (i + 1) + (- (i + 1)) <= (len pn) + (- (i + 1)) by XREAL_1:6;
then A72: ii = (len pn) - (i + 1) by XREAL_0:def 2;
then A73: (len pn) -' ii = (len pn) - ((len pn) - (i + 1)) by XREAL_0:def 2
.= i + 1 ;
S3[(len pn) -' (i + 1)] by A58;
then A74: rng (pn /. ((len pn) -' ii)) c= rng P2 by A66, A72, XBOOLE_1:13;
per cases ( [(((pn /. i1) `1) ^^ <*(t /. i)*>),((pn /. i1) `2)] is consistent or not [(((pn /. i1) `1) ^^ <*(t /. i)*>),((pn /. i1) `2)] is consistent ) ;
suppose A75: [(((pn /. i1) `1) ^^ <*(t /. i)*>),((pn /. i1) `2)] is consistent ; :: thesis: x in rng P2
rng <*(t /. i)*> c= (rng ((pn /. i1) `1)) \/ (rng <*(t /. i)*>) by XBOOLE_1:7;
then rng <*(t /. i)*> c= rng (((pn /. i1) `1) ^ <*(t /. i)*>) by FINSEQ_1:31;
then rng <*(t /. i)*> c= (rng (((pn /. i1) `1) ^ <*(t /. i)*>)) \/ (rng ((pn /. i1) `2)) by XBOOLE_1:10;
then rng <*(t /. i)*> c= (rng (((pn /. i1) `1) ^^ <*(t /. i)*>)) \/ (rng ((pn /. i1) `2)) by A70, Def3;
then rng <*(t /. i)*> c= (rng ((pn /. ((len pn) -' ii)) `1)) \/ (rng ((pn /. i1) `2)) by A73, A75, A33, A65, A67, A68;
then rng <*(t /. i)*> c= rng (pn /. ((len pn) -' ii)) by A75, A33, A65, A67, A68, A73;
then A76: rng <*(t /. i)*> c= rng P2 by A74;
t /. i in {(t /. i)} by TARSKI:def 1;
then t /. i in rng <*(t /. i)*> by FINSEQ_1:38;
then t /. i in rng P2 by A76;
hence x in rng P2 by A62, A63, PARTFUN1:def 6; :: thesis: verum
end;
suppose A77: not [(((pn /. i1) `1) ^^ <*(t /. i)*>),((pn /. i1) `2)] is consistent ; :: thesis: x in rng P2
mg: pn /. ((len pn) -' ii) = [((pn /. i1) `1),(((pn /. i1) `2) ^^ <*(t /. i)*>)] by A77, A33, A65, A67, A68, A73;
rng <*(t /. i)*> c= (rng ((pn /. i1) `2)) \/ (rng <*(t /. i)*>) by XBOOLE_1:7;
then rng <*(t /. i)*> c= rng (((pn /. i1) `2) ^ <*(t /. i)*>) by FINSEQ_1:31;
then rng <*(t /. i)*> c= (rng ((pn /. i1) `1)) \/ (rng (((pn /. i1) `2) ^ <*(t /. i)*>)) by XBOOLE_1:10;
then rng <*(t /. i)*> c= (rng ((pn /. i1) `1)) \/ (rng (((pn /. i1) `2) ^^ <*(t /. i)*>)) by A71, Def3;
then rng <*(t /. i)*> c= (rng ((pn /. i1) `1)) \/ (rng ((pn /. ((len pn) -' ii)) `2)) by mg;
then rng <*(t /. i)*> c= rng (pn /. ((len pn) -' ii)) by mg;
then A78: rng <*(t /. i)*> c= rng P2 by A74;
t /. i in {(t /. i)} by TARSKI:def 1;
then t /. i in rng <*(t /. i)*> by FINSEQ_1:38;
then t /. i in rng P2 by A78;
hence x in rng P2 by A62, A63, PARTFUN1:def 6; :: thesis: verum
end;
end;
end;
suppose A79: x in rng P ; :: thesis: x in rng P2
rng P c= rng (pn /. (len pn)) by A33, A4;
hence x in rng P2 by A79; :: thesis: verum
end;
end;
end;
defpred S4[ Nat] means ( $1 <= len pn implies (rng ((pn /. $1) `1)) \/ (rng ((pn /. $1) `2)) c= tau (rng P) );
A80: (tau (rng P)) \ (rng P) c= tau (rng P) by XBOOLE_1:36;
A81: for k being non zero Nat st S4[k] holds
S4[k + 1]
proof
let k be non zero Nat; :: thesis: ( S4[k] implies S4[k + 1] )
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
A82: 1 <= k by NAT_1:25;
assume A83: S4[k] ; :: thesis: S4[k + 1]
thus S4[k + 1] :: thesis: verum
proof
set P1 = pn /. k1;
set P4 = pn /. k;
assume A84: k + 1 <= len pn ; :: thesis: (rng ((pn /. (k + 1)) `1)) \/ (rng ((pn /. (k + 1)) `2)) c= tau (rng P)
then A85: (k + 1) + (- 1) <= ((len t) + 1) + (- 1) by A4, XREAL_1:6;
then A86: rng ((pn /. k1) `2) misses rng <*(t /. k)*> by A35, A82;
A87: rng ((pn /. k1) `1) misses rng <*(t /. k)*> by A35, A82, A85;
k < len pn by A84, NAT_1:13;
then A88: pn /. k1 is consistent by A33;
A89: {(t /. k1)} c= tau (rng P)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(t /. k1)} or x in tau (rng P) )
A90: k1 in dom t by FINSEQ_3:25, A82, A85;
then t . k1 in rng t by FUNCT_1:3;
then A91: t /. k1 in rng t by PARTFUN1:def 6, A90;
assume x in {(t /. k1)} ; :: thesis: x in tau (rng P)
then x in rng t by A91, TARSKI:def 1;
hence x in tau (rng P) by A1, A80; :: thesis: verum
end;
per cases ( [(((pn /. k1) `1) ^^ <*(t /. k1)*>),((pn /. k1) `2)] is consistent or not [(((pn /. k1) `1) ^^ <*(t /. k1)*>),((pn /. k1) `2)] is consistent ) ;
suppose A92: [(((pn /. k1) `1) ^^ <*(t /. k1)*>),((pn /. k1) `2)] is consistent ; :: thesis: (rng ((pn /. (k + 1)) `1)) \/ (rng ((pn /. (k + 1)) `2)) c= tau (rng P)
set P3 = pn /. (k1 + 1);
A93: pn /. (k1 + 1) = [(((pn /. k1) `1) ^^ <*(t /. k1)*>),((pn /. k1) `2)] by A92, A85, A4, A82, A88;
then A94: rng ((pn /. (k1 + 1)) `2) = rng ((pn /. k) `2) ;
rng ((pn /. (k1 + 1)) `1) = rng (((pn /. k1) `1) ^^ <*(t /. k1)*>) by A93
.= rng (((pn /. k1) `1) ^ <*(t /. k1)*>) by A87, Def3
.= (rng ((pn /. k1) `1)) \/ (rng <*(t /. k1)*>) by FINSEQ_1:31
.= (rng ((pn /. k) `1)) \/ {(t /. k1)} by FINSEQ_1:38 ;
then rng (pn /. (k1 + 1)) = (rng (pn /. k)) \/ {(t /. k1)} by XBOOLE_1:4, A94;
hence (rng ((pn /. (k + 1)) `1)) \/ (rng ((pn /. (k + 1)) `2)) c= tau (rng P) by XBOOLE_1:8, A89, A83, A84, NAT_1:13; :: thesis: verum
end;
suppose A95: not [(((pn /. k1) `1) ^^ <*(t /. k1)*>),((pn /. k1) `2)] is consistent ; :: thesis: (rng ((pn /. (k + 1)) `1)) \/ (rng ((pn /. (k + 1)) `2)) c= tau (rng P)
set P3 = pn /. (k1 + 1);
A96: pn /. (k1 + 1) = [((pn /. k1) `1),(((pn /. k1) `2) ^^ <*(t /. k1)*>)] by A95, A85, A4, A82, A88;
then A97: rng ((pn /. (k1 + 1)) `1) = rng ((pn /. k) `1) ;
rng ((pn /. (k1 + 1)) `2) = rng (((pn /. k1) `2) ^^ <*(t /. k1)*>) by A96
.= rng (((pn /. k1) `2) ^ <*(t /. k1)*>) by Def3, A86
.= (rng ((pn /. k1) `2)) \/ (rng <*(t /. k1)*>) by FINSEQ_1:31
.= (rng ((pn /. k) `2)) \/ {(t /. k1)} by FINSEQ_1:38 ;
then rng (pn /. (k1 + 1)) = (rng (pn /. k)) \/ {(t /. k1)} by A97, XBOOLE_1:4;
hence (rng ((pn /. (k + 1)) `1)) \/ (rng ((pn /. (k + 1)) `2)) c= tau (rng P) by XBOOLE_1:8, A89, A83, A84, NAT_1:13; :: thesis: verum
end;
end;
end;
end;
A98: S4[1] by Th16, A4;
for k being non zero Nat holds S4[k] from NAT_1:sch 10(A98, A81);
 then rng (pn /. lpn) c= tau (rng P) ;
hence ex P1 being consistent PNPair st
( rng (P `1) c= rng (P1 `1) & rng (P `2) c= rng (P1 `2) & tau (rng P) = rng P1 ) by A34, A4, A59, XREAL_0:def 2, A60, XBOOLE_0:def 10; :: thesis: verum