let F be non empty finite set ; :: thesis:
let A be non-empty non empty FinSequence of bool F; :: thesis:
let f be Function; :: thesis:

hereby :: thesis:

assume f is Singlification of A ; :: thesis:
then reconsider f9 = f as Singlification of A ;
f9 is Reduction of A ;
hence dom f = dom A by Def6; :: thesis:
let i be Element of NAT ; :: thesis:
assume A1: i in dom A ; :: thesis:
then ( card (f9 . i) = 1 & A . i <> {} ) by Def8;
hence f is Singlification of A,i by A1, Def7; :: thesis:

end;

assume that
A2: dom f = dom A and
A3: for i being Element of NAT st i in dom A holds
f is Singlification of A,i ; :: thesis:
reconsider f = f as FinSequence of bool F by A3, FINSEQ_5:6;
for i being Element of NAT st i in dom A holds
f . i c= A . i

let i be Element of NAT ; :: thesis:
assume A4: i in dom A ; :: thesis:
then f is Singlification of A,i by A3;
hence f . i c= A . i by A4, Def6; :: thesis:

end;

then reconsider f9 = f as Reduction of A by A2, Def6;
for i being Element of NAT st i in dom A holds
card (f9 . i) = 1

let i be Element of NAT ; :: thesis:
assume A5: i in dom A ; :: thesis:
then ( f is Singlification of A,i & A . i <> {} ) by A3;
hence card (f9 . i) = 1 by A5, Def7; :: thesis:

end;

hence f is Singlification of A by Def8; :: thesis: