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 being Assign of (BASSModel (R,BASSIGN)) holds Tau ((SIGMA f),R,BASSIGN) = f
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds Tau ((SIGMA f),R,BASSIGN) = f
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f being Assign of (BASSModel (R,BASSIGN)) holds Tau ((SIGMA f),R,BASSIGN) = f
let f be Assign of (BASSModel (R,BASSIGN)); :: thesis: Tau ((SIGMA f),R,BASSIGN) = f
set T = SIGMA f;
set g = Tau ((SIGMA f),R,BASSIGN);
A1: SIGMA f = { s where s is Element of S : (Fid (f,S)) . s = TRUE } by Lm40;
for s being object st s in S holds
(Fid (f,S)) . s = (Fid ((Tau ((SIGMA f),R,BASSIGN)),S)) . s

proof

let s be object ; :: thesis: ( s in S implies (Fid (f,S)) . s = (Fid ((Tau ((SIGMA f),R,BASSIGN)),S)) . s )
assume s in S ; :: thesis: (Fid (f,S)) . s = (Fid ((Tau ((SIGMA f),R,BASSIGN)),S)) . s
then reconsider s = s as Element of S ;

per cases ( s in SIGMA f or not s in SIGMA f ) ;

suppose A2: s in SIGMA f ; :: thesis: (Fid (f,S)) . s = (Fid ((Tau ((SIGMA f),R,BASSIGN)),S)) . s

A3: (Fid ((Tau ((SIGMA f),R,BASSIGN)),S)) . s = (chi ((SIGMA f),S)) . s by Def64
.= 1 by A2, FUNCT_3:def 3 ;
ex x being Element of S st
( x = s & (Fid (f,S)) . x = TRUE ) by A1, A2;
hence (Fid (f,S)) . s = (Fid ((Tau ((SIGMA f),R,BASSIGN)),S)) . s by A3; :: thesis: verum

end;

suppose A4: not s in SIGMA f ; :: thesis: (Fid (f,S)) . s = (Fid ((Tau ((SIGMA f),R,BASSIGN)),S)) . s

A5: (Fid (f,S)) . s = FALSE

proof

assume (Fid (f,S)) . s <> FALSE ; :: thesis: contradiction
then (Fid (f,S)) . s = TRUE by TARSKI:def 2;
hence contradiction by A1, A4; :: thesis: verum

end;

(Fid ((Tau ((SIGMA f),R,BASSIGN)),S)) . s = (chi ((SIGMA f),S)) . s by Def64
.= 0 by A4, FUNCT_3:def 3 ;
hence (Fid (f,S)) . s = (Fid ((Tau ((SIGMA f),R,BASSIGN)),S)) . s by A5; :: thesis: verum

end;

end;

end;

hence Tau ((SIGMA f),R,BASSIGN) = f by Lm42, FUNCT_2:12; :: thesis: verum