let P be set ; :: thesis: for F being FinSequence st P is cup-closed & {} in P & ( for n being Nat st n in dom F holds
F . n in P ) holds
Union F in P
let F be FinSequence; :: thesis: ( P is cup-closed & {} in P & ( for n being Nat st n in dom F holds
F . n in P ) implies Union F in P )
assume that
A0: P is cup-closed and
A1: {} in P and
A2: for n being Nat st n in dom F holds
F . n in P ; :: thesis: Union F in P
defpred S₁[ Nat] means union (rng (F | $1)) in P;
A3: S₁[ 0 ] by A1, ZFMISC_1:2;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
A6: k <= k + 1 by NAT_1:13;

per cases ( len F >= k + 1 or len F < k + 1 ) ;

suppose A7: len F >= k + 1 ; :: thesis: S₁[k + 1]

then len (F | (k + 1)) = k + 1 by FINSEQ_1:59;
then F | (k + 1) = ((F | (k + 1)) | k) ^ <*((F | (k + 1)) . (k + 1))*> by FINSEQ_3:55
.= (F | k) ^ <*((F | (k + 1)) . (k + 1))*> by A6, FINSEQ_1:82
.= (F | k) ^ <*(F . (k + 1))*> by FINSEQ_3:112 ;
then rng (F | (k + 1)) = (rng (F | k)) \/ (rng <*(F . (k + 1))*>) by FINSEQ_1:31
.= (rng (F | k)) \/ {(F . (k + 1))} by FINSEQ_1:38 ;
then A8: union (rng (F | (k + 1))) = (union (rng (F | k))) \/ (union {(F . (k + 1))}) by ZFMISC_1:78
.= (union (rng (F | k))) \/ (F . (k + 1)) by ZFMISC_1:25 ;
1 <= k + 1 by NAT_1:11;
then F . (k + 1) in P by A2, A7, FINSEQ_3:25;
hence S₁[k + 1] by A0, A5, A8, FINSUB_1:def 1; :: thesis: verum

end;

suppose len F < k + 1 ; :: thesis: S₁[k + 1]

then ( F | (k + 1) = F & F | k = F ) by FINSEQ_3:49, NAT_1:13;
hence S₁[k + 1] by A5; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
then union (rng (F | (len F))) in P ;
then union (rng F) in P by FINSEQ_3:49;
hence Union F in P by CARD_3:def 4; :: thesis: verum