let X be finite set ; :: thesis: JaccardDist X = SteinhausGen ((SymmetricDiffDist X),({} X))
set f = JaccardDist X;
set g = SteinhausGen ((SymmetricDiffDist X),({} X));
for x being Element of [:(bool X),(bool X):] holds (JaccardDist X) . x = (SteinhausGen ((SymmetricDiffDist X),({} X))) . x

proof

let x be Element of [:(bool X),(bool X):]; :: thesis: (JaccardDist X) . x = (SteinhausGen ((SymmetricDiffDist X),({} X))) . x
consider x1, x2 being object such that
T1: ( x1 in bool X & x2 in bool X & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Subset of X by T1;
set h = SymmetricDiffDist X;
set p = {} X;
V1: (SymmetricDiffDist X) . (x1,({} X)) = card (x1 \+\ ({} X)) by SymDist
.= card x1 ;
V2: (SymmetricDiffDist X) . (x2,({} X)) = card (x2 \+\ ({} X)) by SymDist
.= card x2 ;
V3: (SymmetricDiffDist X) . (x1,x2) = card (x1 \+\ x2) by SymDist;
nn: (SteinhausGen ((SymmetricDiffDist X),({} X))) . (x1,x2) = (2 * (card (x1 \+\ x2))) / (((card x1) + (card x2)) + (card (x1 \+\ x2))) by V3, V2, V1, SteinGen;
(JaccardDist X) . (x1,x2) = (card (x1 \+\ x2)) / (card (x1 \/ x2)) by Similar2
.= (SteinhausGen ((SymmetricDiffDist X),({} X))) . (x1,x2) by HoHo, nn ;
hence (JaccardDist X) . x = (SteinhausGen ((SymmetricDiffDist X),({} X))) . x by T1; :: thesis: verum

end;

hence JaccardDist X = SteinhausGen ((SymmetricDiffDist X),({} X)) ; :: thesis: verum