let S be non empty set ; for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) st Fid (f,S) = Fid (g,S) holds
f = g
let R be total Relation of S,S; for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) st Fid (f,S) = Fid (g,S) holds
f = g
let BASSIGN be non empty Subset of (ModelSP S); for f, g being Assign of (BASSModel (R,BASSIGN)) st Fid (f,S) = Fid (g,S) holds
f = g
let f, g be Assign of (BASSModel (R,BASSIGN)); ( Fid (f,S) = Fid (g,S) implies f = g )
Fid (f,S) = f
by Def41;
hence
( Fid (f,S) = Fid (g,S) implies f = g )
by Def41; verum