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
Cut A,i,x is Reduction of A,i
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
Cut A,i,x is Reduction of A,i
let i be Element of NAT ; :: thesis: for x being set st i in dom A & x in A . i holds
Cut A,i,x is Reduction of A,i
let x be set ; :: thesis: ( i in dom A & x in A . i implies Cut A,i,x is Reduction of A,i )
set f = Cut A,i,x;
assume A1: ( i in dom A & x in A . i ) ; :: thesis: Cut A,i,x is Reduction of A,i
A2: dom (Cut A,i,x) = dom A by Def2;
then A3: for j being Element of NAT st j in dom A & j <> i holds
A . j = (Cut A,i,x) . j by Def2;
(Cut A,i,x) . i = (A . i) \ {x} by A1, A2, Def2;
hence Cut A,i,x is Reduction of A,i by A2, A3, Def5; :: thesis: verum