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

proof

let i be Element of NAT ; :: thesis: ( i in dom A implies C . i c= A . i )
assume A2: i in dom A ; :: thesis: C . i c= A . i
then i in dom B by Def6;
then A3: C . i c= B . i by Def6;
B . i c= A . i by A2, Def6;
hence C . i c= A . i by A3; :: thesis: verum

end;

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