let F, G be Probability of Trivial-SigmaField E; :: thesis: ( ( for A being Event of E holds F . A = prob A ) & ( for A being Event of E holds G . A = prob A ) implies F = G )
assume A9: for A being Event of E holds F . A = prob A ; :: thesis: ( ex A being Event of E st not G . A = prob A or F = G )
assume A10: for A being Event of E holds G . A = prob A ; :: thesis: F = G

now :: thesis: for x being object st x in Trivial-SigmaField E holds
F . x = G . x

let x be object ; :: thesis: ( x in Trivial-SigmaField E implies F . x = G . x )
assume x in Trivial-SigmaField E ; :: thesis: F . x = G . x
then reconsider A = x as Event of E ;
thus F . x = prob A by A9
.= G . x by A10 ; :: thesis: verum

end;

hence F = G by FUNCT_2:12; :: thesis: verum