let Y be non empty finite set ; :: thesis: for s being FinSequence of Y st Y = {1} & s = <*1*> holds
FDprobSEQ s = <*1*>
let s be FinSequence of Y; :: thesis: ( Y = {1} & s = <*1*> implies FDprobSEQ s = <*1*> )
assume A1: ( Y = {1} & s = <*1*> ) ; :: thesis: FDprobSEQ s = <*1*>
A2: ( dom s = {1} & s . 1 = 1 ) by A1, FINSEQ_1:2, FINSEQ_1:def 8;
A3: ( len s = 1 & card Y = 1 ) by A1, CARD_1:30;
A4: dom s = Seg (card Y) by A2, A1, CARD_1:30, FINSEQ_1:2;
rng s = {1} by A1, FINSEQ_1:39;
then A5: 1 in rng s by TARSKI:def 1;
A6: FDprobability (((canFS Y) . 1),s) = FDprobability ((<*1*> . 1),s) by A1, FINSEQ_1:94
.= FDprobability (1,s) by FINSEQ_1:def 8
.= 1 by A1, A5, A3, FINSEQ_4:73 ;
for n being Nat st n in dom s holds
s . n = FDprobability (((canFS Y) . n),s)
proof
let n be Nat; :: thesis: ( n in dom s implies s . n = FDprobability (((canFS Y) . n),s) )
assume n in dom s ; :: thesis: s . n = FDprobability (((canFS Y) . n),s)
then n = 1 by A2, TARSKI:def 1;
hence s . n = FDprobability (((canFS Y) . n),s) by A6, A1, FINSEQ_1:def 8; :: thesis: verum
end;
hence FDprobSEQ s = <*1*> by A4, A1, DIST_1:def 3; :: thesis: verum