let F be finite set ; :: thesis: for A being FinSequence of bool F
for i being Element of NAT
for C being Reduction of A,i holds C is Reduction of A
let A be FinSequence of bool F; :: thesis: for i being Element of NAT
for C being Reduction of A,i holds C is Reduction of A
let i be Element of NAT ; :: thesis: for C being Reduction of A,i holds C is Reduction of A
let C be Reduction of A,i; :: thesis: C is Reduction of A
A1: dom C = dom A by Def5;
for j being Element of NAT st j in dom C holds
C . j c= A . j

proof

let j be Element of NAT ; :: thesis: ( j in dom C implies C . j c= A . j )
assume A2: j in dom C ; :: thesis: C . j c= A . j

per cases ( j = i or j <> i ) ;

suppose j = i ; :: thesis: C . j c= A . j

hence C . j c= A . j by Def5; :: thesis: verum

end;

suppose j <> i ; :: thesis: C . j c= A . j

hence C . j c= A . j by A1, A2, Def5; :: thesis: verum

end;

end;

end;

hence C is Reduction of A by A1, Def6; :: thesis: verum