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 A1: ( i in dom A & x in A . i ) ; :: thesis: card ((Cut A,i,x) . i) = (card (A . i)) - 1
then A2: {x} c= A . i by ZFMISC_1:37;
i in dom (Cut A,i,x) by A1, Def2;
then (Cut A,i,x) . i = (A . i) \ {x} by Def2;
then card ((Cut A,i,x) . i) = (card (A . i)) - (card {x}) by A2, CARD_2:63
.= (card (A . i)) - 1 by CARD_2:60 ;
hence card ((Cut A,i,x) . i) = (card (A . i)) - 1 ; :: thesis: verum