let F be finite set ; :: thesis: for A being FinSequence of bool F
for i being Element of NAT
for x being set st i in dom A & x in A . i holds
card ((Cut A,i,x) . i) = (card (A . i)) - 1
let A be FinSequence of bool F; :: thesis: for i being Element of NAT
for x being set st i in dom A & x in A . i holds
card ((Cut A,i,x) . i) = (card (A . i)) - 1
let i be Element of NAT ; :: thesis: for x being set st i in dom A & x in A . i holds
card ((Cut A,i,x) . i) = (card (A . i)) - 1
let x be set ; :: thesis: ( i in dom A & x in A . i implies card ((Cut A,i,x) . i) = (card (A . i)) - 1 )
set f = Cut A,i,x;
assume that
A1: i in dom A and
A2: x in A . i ; :: thesis: card ((Cut A,i,x) . i) = (card (A . i)) - 1
i in dom (Cut A,i,x) by A1, Def2;
then A3: (Cut A,i,x) . i = (A . i) \ {x} by Def2;
{x} c= A . i by A2, ZFMISC_1:37;
then card ((Cut A,i,x) . i) = (card (A . i)) - (card {x}) by A3, CARD_2:63
.= (card (A . i)) - 1 by CARD_2:60 ;
hence card ((Cut A,i,x) . i) = (card (A . i)) - 1 ; :: thesis: verum