let F be set ; :: thesis: for A being FinSequence of bool F
for i being Element of NAT holds A is Reduction of A,i
let A be FinSequence of bool F; :: thesis: for i being Element of NAT holds A is Reduction of A,i
let i be Element of NAT ; :: thesis: A is Reduction of A,i
( ( for j being Element of NAT st j in dom A & j <> i holds
A . j = A . j ) & A . i c= A . i ) ;
hence A is Reduction of A,i by Def5; :: thesis: verum