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
C1: f1 in ModelSP S and
C2: f2 in ModelSP S ; :: thesis: ( not Fid f1,S = Fid f2,S or f1 = f2 )
assume C3: Fid f1,S = Fid f2,S ; :: thesis: f1 = f2
Fid f1,S = f1 by C1, MODELC_1:def 41;
hence f1 = f2 by C2, C3, MODELC_1:def 41; :: thesis: verum