let F be non empty finite set ; :: thesis: for A being non empty FinSequence of bool F
for X being set
for B being Reduction of A st X is_a_system_of_different_representatives_of B holds
X is_a_system_of_different_representatives_of A
let A be non empty FinSequence of bool F; :: thesis: for X being set
for B being Reduction of A st X is_a_system_of_different_representatives_of B holds
X is_a_system_of_different_representatives_of A
let X be set ; :: thesis: for B being Reduction of A st X is_a_system_of_different_representatives_of B holds
X is_a_system_of_different_representatives_of A
let B be Reduction of A; :: thesis: ( X is_a_system_of_different_representatives_of B implies X is_a_system_of_different_representatives_of A )
assume A1: X is_a_system_of_different_representatives_of B ; :: thesis: X is_a_system_of_different_representatives_of A
X is_a_system_of_different_representatives_of A

proof

consider f being FinSequence of F such that
A2: ( f = X & dom B = dom f & ( for i being Element of NAT st i in dom f holds
f . i in B . i ) & f is one-to-one ) by A1, Def3;
A3: dom A = dom B by Def6;
for i being Element of NAT st i in dom f holds
f . i in A . i

proof

let i be Element of NAT ; :: thesis: ( i in dom f implies f . i in A . i )
assume A4: i in dom f ; :: thesis: f . i in A . i
f . i in A . i

proof

A5: f . i in B . i by A2, A4;
( dom B = dom A & ( for i being Element of NAT st i in dom A holds
B . i c= A . i ) ) by Def6;
then B . i c= A . i by A2, A4;
hence f . i in A . i by A5; :: thesis: verum

end;

hence f . i in A . i ; :: thesis: verum

end;

hence X is_a_system_of_different_representatives_of A by A2, A3, Def3; :: thesis: verum

end;

hence X is_a_system_of_different_representatives_of A ; :: thesis: verum