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
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
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
let x be set ; :: thesis: ( i in dom A & x in A . i implies Cut A,i,x is Reduction of A )
assume ( i in dom A & x in A . i ) ; :: thesis: 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; :: thesis: verum