let g, h be FinSequence of NAT ; :: thesis: ( dom g = Seg (card S) & ( for n being Nat st n in dom g holds
g . n = (len s) * ((FDprobSEQ s) . n) ) & dom h = Seg (card S) & ( for n being Nat st n in dom h holds
h . n = (len s) * ((FDprobSEQ s) . n) ) implies g = h )
assume that
A8: dom g = Seg (card S) and
A9: for n being Nat st n in dom g holds
g . n = (len s) * ((FDprobSEQ s) . n) ; :: thesis: ( not dom h = Seg (card S) or ex n being Nat st
( n in dom h & not h . n = (len s) * ((FDprobSEQ s) . n) ) or g = h )
assume that
A10: dom h = Seg (card S) and
A11: for n being Nat st n in dom h holds
h . n = (len s) * ((FDprobSEQ s) . n) ; :: thesis: g = h

A12: now

let n be Nat; :: thesis: ( n in dom g implies g . n = h . n )
assume A13: n in dom g ; :: thesis: g . n = h . n
hence g . n = (len s) * ((FDprobSEQ s) . n) by A9
.= h . n by A8, A10, A11, A13 ;
:: thesis: verum

end;

len g = card S by A8, FINSEQ_1:def 3
.= len h by A10, FINSEQ_1:def 3 ;
hence g = h by A12, FINSEQ_2:9; :: thesis: verum