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 43;
hence f1 = f2 by A2, A3, MODELC_1:def 43; :: thesis: verum