let F be finite set ; for A being FinSequence of bool F
for i being Element of NAT
for x being set st i in dom A holds
Cut (A,i,x) is Reduction of A
let A be FinSequence of bool F; for i being Element of NAT
for x being set st i in dom A holds
Cut (A,i,x) is Reduction of A
let i be Element of NAT ; for x being set st i in dom A holds
Cut (A,i,x) is Reduction of A
let x be set ; ( i in dom A implies Cut (A,i,x) is Reduction of A )
assume
i in dom A
; Cut (A,i,x) is Reduction of A
then
Cut (A,i,x) is Reduction of A,i
by Th20;
hence
Cut (A,i,x) is Reduction of A
by Th19; verum