let m be Nat; :: thesis: ( m <> 0 implies 2 * (card (bool ((Seg m) \ {1}))) = card (bool ((Seg (1 + m)) \ {1})) )
assume A1: m <> 0 ; :: thesis: 2 * (card (bool ((Seg m) \ {1}))) = card (bool ((Seg (1 + m)) \ {1}))
set S = (Seg m) \ {1};
set F = bool ((Seg m) \ {1});
{} misses union (bool ((Seg m) \ {1})) ;
then A2: card (UNION ((bool ((Seg m) \ {1})),{{}})) = card (bool ((Seg m) \ {1})) by Th8;
{(m + 1)} misses union (bool ((Seg m) \ {1}))

proof

assume {(m + 1)} meets union (bool ((Seg m) \ {1})) ; :: thesis: contradiction
then consider x being object such that
A3: ( x in {(m + 1)} & x in union (bool ((Seg m) \ {1})) ) by XBOOLE_0:3;
( x = m + 1 & x in (Seg m) \ {1} ) by A3, TARSKI:def 1;
then m + 1 in Seg m by XBOOLE_0:def 5;
then m + 1 <= m by FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum

end;

then A4: card (UNION ((bool ((Seg m) \ {1})),{{(m + 1)}})) = card (bool ((Seg m) \ {1})) by Th8;
( {{}} \/ {{(m + 1)}} = {{},{(m + 1)}} & {{},{(m + 1)}} = bool {(m + 1)} ) by ENUMSET1:1, ZFMISC_1:24;
then A5: UNION ((bool ((Seg m) \ {1})),(bool {(m + 1)})) = (UNION ((bool ((Seg m) \ {1})),{{}})) \/ (UNION ((bool ((Seg m) \ {1})),{{(m + 1)}})) by Th7;
UNION ((bool ((Seg m) \ {1})),{{}}) misses UNION ((bool ((Seg m) \ {1})),{{(m + 1)}})

proof

assume UNION ((bool ((Seg m) \ {1})),{{}}) meets UNION ((bool ((Seg m) \ {1})),{{(m + 1)}}) ; :: thesis: contradiction
then consider x being object such that
A6: ( x in UNION ((bool ((Seg m) \ {1})),{{}}) & x in UNION ((bool ((Seg m) \ {1})),{{(m + 1)}}) ) by XBOOLE_0:3;
consider a, b being set such that
A7: ( a in bool ((Seg m) \ {1}) & b in {{}} & x = a \/ b ) by A6, SETFAM_1:def 4;
consider c, d being set such that
A8: ( c in bool ((Seg m) \ {1}) & d in {{(m + 1)}} & x = c \/ d ) by A6, SETFAM_1:def 4;
( b = {} & m + 1 in {(m + 1)} & {(m + 1)} = d ) by A7, A8, TARSKI:def 1;
then ( m + 1 in c \/ d & c \/ d = a ) by A7, A8, XBOOLE_0:def 3;
then m + 1 in Seg m by XBOOLE_0:def 5, A7;
then m + 1 <= m by FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum

end;

then A9: card (UNION ((bool ((Seg m) \ {1})),(bool {(m + 1)}))) = (card (UNION ((bool ((Seg m) \ {1})),{{}}))) + (card (UNION ((bool ((Seg m) \ {1})),{{(m + 1)}}))) by A5, CARD_2:40;
1 <> 1 + m by A1;
then A10: {(1 + m)} \ {1} = {(1 + m)} by ZFMISC_1:14;
Seg (1 + m) = (Seg m) \/ {(1 + m)} by FINSEQ_1:9;
then (Seg (1 + m)) \ {1} = ((Seg m) \ {1}) \/ {(1 + m)} by A10, XBOOLE_1:42;
hence 2 * (card (bool ((Seg m) \ {1}))) = card (bool ((Seg (1 + m)) \ {1})) by A2, A4, A9, Th6; :: thesis: verum