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 SIGMA f = SIGMA g 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 SIGMA f = SIGMA g holds
f = g
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g being Assign of (CTLModel R,BASSIGN) st SIGMA f = SIGMA g holds
f = g
let f, g be Assign of (CTLModel R,BASSIGN); :: thesis: ( SIGMA f = SIGMA g implies f = g )
assume A1: SIGMA f = SIGMA g ; :: thesis: f = g
SIGMA f = { s where s is Element of S : (Fid f,S) . s = TRUE } by Lm46;
then { s where s is Element of S : (Fid f,S) . s = TRUE } = { s where s is Element of S : (Fid g,S) . s = TRUE } by A1, Lm46;
hence f = g by Lm47, Lm48; :: thesis: verum