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 S_{1}[ 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)*>)] ) ) );

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

S_{1}[n,pn /. n,pn /. (n + 1)] ) )
from RECDEF_1:sch 18(A3);

defpred S_{2}[ 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 S_{2}[k] holds

S_{2}[k + 1]

A31: S_{2}[1]
_{2}[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 S_{3}[ 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) ) );

_{3}[ 0 ]
_{3}[n]
from NAT_1:sch 2(A57, A39);

then A59: ( (len pn) + (- 1) < len pn & S_{3}[(len pn) -' 1] )
by XREAL_1:30;

A60: tau (rng P) c= rng P2_{4}[ 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 S_{4}[k] holds

S_{4}[k + 1]
_{4}[1]
by Th16, A4;

for k being non zero Nat holds S_{4}[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

( 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 S

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 S_{1}[n,x,y]

consider pn being FinSequence of [:(LTLB_WFF **),(LTLB_WFF **):] such that for x being Element of [:(LTLB_WFF **),(LTLB_WFF **):] ex y being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st S

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 S_{1}[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 S_{1}[n,x,y]

let x be Element of [:(LTLB_WFF **),(LTLB_WFF **):]; :: thesis: ex y being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st S_{1}[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 S_{1}[n,x,y]
; :: thesis: verum

end;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 S

let x be Element of [:(LTLB_WFF **),(LTLB_WFF **):]; :: thesis: ex y being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st S

( [((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 S

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

S

defpred S

A5: for k being non zero Nat st S

S

proof

reconsider lpn = len pn as non zero Nat by A4;
let k be non zero Nat; :: thesis: ( S_{2}[k] implies S_{2}[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: S_{2}[k]
; :: thesis: S_{2}[k + 1]

A9: 1 <= k + 1 by NAT_1:25;

thus S_{2}[k + 1]
:: thesis: verum

end;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: S

A9: 1 <= k + 1 by NAT_1:25;

thus S

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: S_{1}[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)*>)];

end;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: S

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 )
;

end;

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)) )

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;.= (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

thus
pn /. (k + 1) is consistent
by A4, A6, A17, A20; :: thesis: rng P c= rng (pn /. (k + 1))
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;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

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

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)) )

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;.= (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

thus
pn /. (k + 1) is consistent
by A19, Th31, A16; :: thesis: rng P c= rng (pn /. (k + 1))
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;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

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

A31: S

proof

A33:
for k being non zero Nat holds S
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) )

thus rng P c= rng (pn /. 1) by A4; :: thesis: verum

end;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

thus
pn /. 1 is consistent
by A4; :: thesis: rng P c= rng (pn /. 1)
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;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

thus rng P c= rng (pn /. 1) by A4; :: thesis: verum

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 S

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)*> )

( 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;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

A39: now :: thesis: for n being Nat st S_{3}[n] holds

S_{3}[n + 1]

A57:
SS

let n be Nat; :: thesis: ( S_{3}[n] implies S_{3}[n + 1] )

set k = (len pn) -' (n + 1);

assume A40: S_{3}[n]
; :: thesis: S_{3}[n + 1]

thus S_{3}[n + 1]
:: thesis: verum

end;set k = (len pn) -' (n + 1);

assume A40: S

thus S

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;

end;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 )
;

end;

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;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

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;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

proof

A58:
for n being Nat holds S
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;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

then A59: ( (len pn) + (- 1) < len pn & S

A60: tau (rng P) c= rng P2

proof

defpred S
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;

end;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;

end;

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: S_{1}[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 ;

S_{3}[(len pn) -' (i + 1)]
by A58;

then A74: rng (pn /. ((len pn) -' ii)) c= rng P2 by A66, A72, XBOOLE_1:13;

end;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: S

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 ;

S

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 )
;

end;

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;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

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;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

A80: (tau (rng P)) \ (rng P) c= tau (rng P) by XBOOLE_1:36;

A81: for k being non zero Nat st S

S

proof

A98:
S
let k be non zero Nat; :: thesis: ( S_{4}[k] implies S_{4}[k + 1] )

reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

A82: 1 <= k by NAT_1:25;

assume A83: S_{4}[k]
; :: thesis: S_{4}[k + 1]

thus S_{4}[k + 1]
:: thesis: verum

end;reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

A82: 1 <= k by NAT_1:25;

assume A83: S

thus S

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)

end;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;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

per cases
( [(((pn /. k1) `1) ^^ <*(t /. k1)*>),((pn /. k1) `2)] is consistent or not [(((pn /. k1) `1) ^^ <*(t /. k1)*>),((pn /. k1) `2)] is consistent )
;

end;

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;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

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;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

for k being non zero Nat holds S

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