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 ;
defpred S1[ Nat, Element of [:(),():], Element of [:(),():]] 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 [:(),():] ex y being Element of [:(),():] st S1[n,x,y]
let n be Nat; :: thesis: ( 1 <= n & n <= ((len t) + 1) - 1 implies for x being Element of [:(),():] ex y being Element of [:(),():] st S1[n,x,y] )
assume that
1 <= n and
n <= ((len t) + 1) - 1 ; :: thesis: for x being Element of [:(),():] ex y being Element of [:(),():] st S1[n,x,y]
let x be Element of [:(),():]; :: thesis: ex y being Element of [:(),():] 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 [:(),():] st S1[n,x,y] ; :: thesis: verum
end;
consider pn being FinSequence of [:(),():] 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 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 ;
set pp = [((P1 `1) ^^ <*(t /. k1)*>),(P1 `2)];
set pp2 = [(P1 `1),((P1 `2) ^^ <*(t /. k1)*>)];
A12: rng P1 misses rng (t /^ k1) by ;
rng P1 misses rng <*(t /. k1)*> by ;
then A13: rng (P1 `2) misses rng <*(t /. k1)*> by ;
A14: rng P1 misses rng <*(t /. k1)*> by ;
then A15: rng (P1 `1) misses rng <*(t /. k1)*> by ;
(rng P1) /\ (rng <*(t /. k1)*>) = {} by A14;
then A16: not t /. k1 in rng P1 by ;
A17: (k + 1) + (- 1) <= ((len t) + 1) + (- 1) by ;
then A18: k in dom t by ;
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
.= ((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 ;
then {(t /. (k + 1))} c= rng (t /^ k) by ;
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 ;
k1 in Seg k1 by A6;
then t . k1 in rng (t | (Seg k)) by ;
then t /. k1 in rng (t | k) by ;
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 ;
(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
.= {} \/ ((rng <*(t /. k1)*>) /\ ((rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))))) by
.= {} 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 ;
hence rng P c= rng (pn /. (k + 1)) by ; :: 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
.= (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 ;
then {(t /. (k + 1))} c= rng (t /^ k) by ;
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 ;
k1 in Seg k1 by A6;
then t . k1 in rng (t | (Seg k)) by ;
then t /. k1 in rng (t | k) by ;
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 ;
(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
.= {} \/ ((rng <*(t /. k1)*>) /\ ((rng <*(t /. (k + 1))*>) \/ (rng (t /^ (k + 1))))) by
.= {} 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 ; :: thesis: rng P c= rng (pn /. (k + 1))
rng (pn /. k) c= rng (pn /. (k + 1)) by ;
hence rng P c= rng (pn /. (k + 1)) by ; :: 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
.= rng t by ;
hence rng (pn /. 1) misses (rng <*(t /. 1)*>) \/ (rng (t /^ 1)) by ; :: 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 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
.= (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 ;
then rng (pn /. n) misses (rng <*(t /. n)*>) \/ (rng (t /^ n)) by ;
then A38: rng (pn /. n) misses rng <*(t /. n)*> by ;
hence rng ((pn /. n) `1) misses rng <*(t /. n)*> by ; :: thesis: rng ((pn /. n) `2) misses rng <*(t /. n)*>
thus rng ((pn /. n) `2) misses rng <*(t /. n)*> by ; :: 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 ;
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 ;
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 ;
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 ;
k < len pn by ;
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 ;
then rng (((pn /. k) `1) ^ <*(t /. k)*>) c= rng (P2 `1) by ;
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 ;
then rng (((pn /. k) `2) ^ <*(t /. k)*>) c= rng (P2 `2) by ;
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 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 ;
per cases ( x in (tau (rng P)) \ (rng P) or x in rng P ) by ;
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 ;
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
set P5 = pn /. i1;
A64: i <= ((len t) + 1) - 1 by ;
then A65: i < len pn by ;
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 ;
then A68: S1[i1,pn /. i1,pn /. (i1 + 1)] by ;
A69: i <= len t by ;
then A70: rng ((pn /. i1) `1) misses rng <*(t /. i)*> by ;
A71: rng ((pn /. i1) `2) misses rng <*(t /. i)*> by ;
i + 1 <= len pn by ;
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 ;
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 ;
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 ; :: 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 ;
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 ; :: thesis: verum
end;
end;
end;
suppose A79: x in rng P ; :: thesis: x in rng P2
rng P c= rng (pn /. (len pn)) by ;
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 ;
then A86: rng ((pn /. k1) `2) misses rng <*(t /. k)*> by ;
A87: rng ((pn /. k1) `1) misses rng <*(t /. k)*> by ;
k < len pn by ;
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 ;
then t . k1 in rng t by FUNCT_1:3;
then A91: t /. k1 in rng t by ;
assume x in {(t /. k1)} ; :: thesis: x in tau (rng P)
then x in rng t by ;
hence x in tau (rng P) by ; :: 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
.= (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 ;
hence (rng ((pn /. (k + 1)) `1)) \/ (rng ((pn /. (k + 1)) `2)) c= tau (rng P) by ; :: 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
.= (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 ;
hence (rng ((pn /. (k + 1)) `1)) \/ (rng ((pn /. (k + 1)) `2)) c= tau (rng P) by ; :: thesis: verum
end;
end;
end;
end;
A98: S4[1] by Th16, A4;
for k being non zero Nat holds S4[k] from 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 ; :: thesis: verum