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
( dom B = dom C & ( for i being Element of NAT st i in dom B holds
C . i c= B . i ) ) by Def6;
then A1: dom A = dom C by Def6;
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 A3: i in dom B by Def6;
A4: B . i c= A . i by A2, Def6;
C . i c= B . i by A3, Def6;
hence C . i c= A . i by A4, XBOOLE_1:1; :: thesis: verum

end;

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