let S be non empty set ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( not Fid (f1,S) = Fid (f2,S) or f1 = f2 )
assume A3: Fid (f1,S) = Fid (f2,S) ; :: thesis: f1 = f2
Fid (f1,S) = f1 by A1, MODELC_1:def 41;
hence f1 = f2 by A2, A3, MODELC_1:def 41; :: thesis: verum