set A = { F1(i) where i is Nat : i < len F2() } ;
defpred S1[ Nat] means ( $1 <= len F2() implies for f being FinSequence of NAT st len f = $1 & ( for i being Nat st i < $1 holds
card F1(i) = f . (i + 1) ) holds
card (union { F1(i) where i is Nat : i < $1 } ) = Sum f );
A3: S1[ 0 ]
proof
assume 0 <= len F2() ; :: thesis: for f being FinSequence of NAT st len f = 0 & ( for i being Nat st i < 0 holds
card F1(i) = f . (i + 1) ) holds
card (union { F1(i) where i is Nat : i < 0 } ) = Sum f
let f be FinSequence of NAT ; :: thesis: ( len f = 0 & ( for i being Nat st i < 0 holds
card F1(i) = f . (i + 1) ) implies card (union { F1(i) where i is Nat : i < 0 } ) = Sum f )
assume len f = 0 ; :: thesis: ( ex i being Nat st
( i < 0 & not card F1(i) = f . (i + 1) ) or card (union { F1(i) where i is Nat : i < 0 } ) = Sum f )
then reconsider f = f as empty FinSequence of NAT ;
{ F1(i) where i is Nat : i < 0 } c= {}
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { F1(i) where i is Nat : i < 0 } or a in {} )
assume a in { F1(i) where i is Nat : i < 0 } ; :: thesis: a in {}
then ex i being Nat st
( a = F1(i) & i < 0 ) ;
hence a in {} ; :: thesis: verum
end;
then ( { F1(i) where i is Nat : i < 0 } = {} & {} = union {} & Sum f = 0 ) by ZFMISC_1:2, RVSUM_1:72;
hence ( ex i being Nat st
( i < 0 & not card F1(i) = f . (i + 1) ) or card (union { F1(i) where i is Nat : i < 0 } ) = Sum f ) ; :: thesis: verum
end;
A4: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A5: S1[n] ; :: thesis: S1[n + 1]
assume B0: n + 1 <= len F2() ; :: thesis: for f being FinSequence of NAT st len f = n + 1 & ( for i being Nat st i < n + 1 holds
card F1(i) = f . (i + 1) ) holds
card (union { F1(i) where i is Nat : i < n + 1 } ) = Sum f
then B1: n < len F2() by NAT_1:13;
let f be FinSequence of NAT ; :: thesis: ( len f = n + 1 & ( for i being Nat st i < n + 1 holds
card F1(i) = f . (i + 1) ) implies card (union { F1(i) where i is Nat : i < n + 1 } ) = Sum f )
assume A6: ( len f = n + 1 & ( for i being Nat st i < n + 1 holds
card F1(i) = f . (i + 1) ) ) ; :: thesis: card (union { F1(i) where i is Nat : i < n + 1 } ) = Sum f
then consider f1 being FinSequence of NAT , j being Element of NAT such that
A8: f = f1 ^ <*j*> by FINSEQ_2:19;
B5: n < n + 1 by NAT_1:13;
B6: len f = (len f1) + 1 by A8, FINSEQ_2:16;
B2: for i being Nat st i < n holds
card F1(i) = f1 . (i + 1)
proof
let i be Nat; :: thesis: ( i < n implies card F1(i) = f1 . (i + 1) )
assume D1: i < n ; :: thesis: card F1(i) = f1 . (i + 1)
then ( 1 <= i + 1 & i + 1 <= n ) by NAT_1:11, NAT_1:13;
then i + 1 in dom f1 by B6, A6, FINSEQ_3:25;
then ( f . (i + 1) = f1 . (i + 1) & i < n + 1 ) by D1, A8, NAT_1:13, FINSEQ_1:def 7;
hence card F1(i) = f1 . (i + 1) by A6; :: thesis: verum
end;
A7: ( j = f . (n + 1) & f . (n + 1) = card F1(n) ) by B6, B5, A6, A8, FINSEQ_1:42;
B3: union { F1(i) where i is Nat : i < n } misses F1(n)
proof
assume union { F1(i) where i is Nat : i < n } meets F1(n) ; :: thesis: contradiction
then consider a being object such that
C1: ( a in union { F1(i) where i is Nat : i < n } & a in F1(n) ) by XBOOLE_0:3;
consider J being set such that
C2: ( a in J & J in { F1(i) where i is Nat : i < n } ) by C1, TARSKI:def 4;
consider i being Nat such that
C3: ( J = F1(i) & i < n ) by C2;
i < len F2() by B1, C3, XXREAL_0:2;
hence contradiction by A1, B1, C1, C2, C3, XBOOLE_0:3; :: thesis: verum
end;
{ F1(i) where i is Nat : i < n + 1 } = { F1(i) where i is Nat : i < n } \/ {F1(n)}
proof
thus { F1(i) where i is Nat : i < n + 1 } c= { F1(i) where i is Nat : i < n } \/ {F1(n)} :: according to XBOOLE_0:def 10 :: thesis: { F1(i) where i is Nat : i < n } \/ {F1(n)} c= { F1(i) where i is Nat : i < n + 1 }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { F1(i) where i is Nat : i < n + 1 } or a in { F1(i) where i is Nat : i < n } \/ {F1(n)} )
assume a in { F1(i) where i is Nat : i < n + 1 } ; :: thesis: a in { F1(i) where i is Nat : i < n } \/ {F1(n)}
then consider i being Nat such that
C4: ( a = F1(i) & i < n + 1 ) ;
i <= n by C4, NAT_1:13;
then ( i < n or i = n ) by XXREAL_0:1;
then ( a in { F1(j) where j is Nat : j < n } or a in {F1(n)} ) by C4, TARSKI:def 1;
hence a in { F1(i) where i is Nat : i < n } \/ {F1(n)} by XBOOLE_0:def 3; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { F1(i) where i is Nat : i < n } \/ {F1(n)} or a in { F1(i) where i is Nat : i < n + 1 } )
assume a in { F1(i) where i is Nat : i < n } \/ {F1(n)} ; :: thesis: a in { F1(i) where i is Nat : i < n + 1 }
per cases then ( a in { F1(i) where i is Nat : i < n } or a in {F1(n)} ) by XBOOLE_0:def 3;
suppose a in { F1(i) where i is Nat : i < n } ; :: thesis: a in { F1(i) where i is Nat : i < n + 1 }
then consider i being Nat such that
C5: ( a = F1(i) & i < n ) ;
i < n + 1 by NAT_1:13, C5;
hence a in { F1(i) where i is Nat : i < n + 1 } by C5; :: thesis: verum
end;
suppose a in {F1(n)} ; :: thesis: a in { F1(i) where i is Nat : i < n + 1 }
then a = F1(n) by TARSKI:def 1;
hence a in { F1(i) where i is Nat : i < n + 1 } by B5; :: thesis: verum
end;
end;
end;
then union { F1(i) where i is Nat : i < n + 1 } = (union { F1(i) where i is Nat : i < n } ) \/ (union {F1(n)}) by ZFMISC_1:78
.= (union { F1(i) where i is Nat : i < n } ) \/ F1(n) ;
hence card (union { F1(i) where i is Nat : i < n + 1 } ) = (card (union { F1(i) where i is Nat : i < n } )) +` (card F1(n)) by B3, CARD_2:35
.= (Sum f1) +` j by A7, A5, B0, B2, B6, A6, NAT_1:13
.= Sum f by A8, RVSUM_1:74 ;
:: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A3, A4);
 hence card (union { F1(i) where i is Nat : i < len F2() } ) = Sum F2() by A2; :: thesis: verum