consider A1 being SetSequence of REAL such that
A1: for n being Nat holds A1 . n = {n} by Q00;
A2: for n being Nat holds A1 . n is Event of Borel_Sets
proof
let n be Nat; :: thesis: A1 . n is Event of Borel_Sets
reconsider n = n as Element of REAL by NUMBERS:19, ORDINAL1:def 12;
{n} in Borel_Sets by Th1;
hence A1 . n is Event of Borel_Sets by A1; :: thesis: verum
end;
reconsider A1 = A1 as SetSequence of Borel_Sets by PROB_1:25, A2;
take A1 ; :: thesis: for n being Nat holds A1 . n = {n}
thus for n being Nat holds A1 . n = {n} by A1; :: thesis: verum