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 and
A3: dom B = dom f and
A4: for i being Element of NAT st i in dom f holds
f . i in B . i and
A5: f is one-to-one by A1;
A6: 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 A7: i in dom f ; :: thesis: f . i in A . i
A8: f . i in B . i by A4, A7;
dom B = dom A by Def6;
then B . i c= A . i by A3, A7, Def6;
hence f . i in A . i by A8; :: thesis: verum

end;

dom A = dom B by Def6;
hence X is_a_system_of_different_representatives_of A by A2, A3, A5, A6; :: thesis: verum

end;

hence X is_a_system_of_different_representatives_of A ; :: thesis: verum