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 (BASSModel (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 (BASSModel (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 (BASSModel (R,BASSIGN)) st SIGMA f = SIGMA g holds
f = g
let f, g be Assign of (BASSModel (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 Lm40;
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, Lm40;
hence f = g by Lm41, Lm42; :: thesis: verum