let F be non empty finite set ; :: thesis: for A being non empty FinSequence of bool F holds
( ex X being set st X is_a_system_of_different_representatives_of A iff A is Hall )
let A be non empty FinSequence of bool F; :: thesis: ( ex X being set st X is_a_system_of_different_representatives_of A iff A is Hall )
thus ( ex X being set st X is_a_system_of_different_representatives_of A implies A is Hall ) by Th18; :: thesis: ( A is Hall implies ex X being set st X is_a_system_of_different_representatives_of A )
assume A1: A is Hall ; :: thesis: ex X being set st X is_a_system_of_different_representatives_of A
then consider G being Singlification of A such that
A2: G is Hall by Th31;
for i being Element of NAT st i in dom G holds
card (G . i) = 1

proof

let i be Element of NAT ; :: thesis: ( i in dom G implies card (G . i) = 1 )
assume A3: i in dom G ; :: thesis: card (G . i) = 1
dom G = dom A by Def6;
hence card (G . i) = 1 by A1, A3, Def8; :: thesis: verum

end;

then ex X being set st X is_a_system_of_different_representatives_of G by A2, Th17;
hence ex X being set st X is_a_system_of_different_representatives_of A by Th28; :: thesis: verum