let F be set ; :: thesis: for A being FinSequence of bool F holds A is Reduction of A
let A be FinSequence of bool F; :: thesis: A is Reduction of A
for i being Element of NAT st i in dom A holds
A . i c= A . i ;
hence A is Reduction of A by Def6; :: thesis: verum