let S be non empty set ; for f1, f2 being set st f1 in ModelSP S & f2 in ModelSP S & Fid (f1,S) = Fid (f2,S) holds
f1 = f2
let f1, f2 be set ; ( f1 in ModelSP S & f2 in ModelSP S & Fid (f1,S) = Fid (f2,S) implies f1 = f2 )
assume that
A1:
f1 in ModelSP S
and
A2:
f2 in ModelSP S
; ( not Fid (f1,S) = Fid (f2,S) or f1 = f2 )
assume A3:
Fid (f1,S) = Fid (f2,S)
; f1 = f2
Fid (f1,S) = f1
by A1, MODELC_1:def 41;
hence
f1 = f2
by A2, A3, MODELC_1:def 41; verum