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:31;
then card ((Cut (A,i,x)) . i) = (card (A . i)) - (card {x}) by A3, CARD_2:44
.= (card (A . i)) - 1 by CARD_2:42 ;
hence card ((Cut (A,i,x)) . i) = (card (A . i)) - 1 ; :: thesis: verum