let S be non empty set ; :: thesis: for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (CTLModel R,BASSIGN) st Fid f,S = Fid g,S holds
f = g
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (CTLModel R,BASSIGN) st Fid f,S = Fid g,S holds
f = g
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g being Assign of (CTLModel R,BASSIGN) st Fid f,S = Fid g,S holds
f = g
let f, g be Assign of (CTLModel R,BASSIGN); :: thesis: ( 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; :: thesis: verum