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 (CTLModel 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 (CTLModel R,BASSIGN) holds Tau (SIGMA f),R,BASSIGN = f
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f being Assign of (CTLModel R,BASSIGN) holds Tau (SIGMA f),R,BASSIGN = f
let f be Assign of (CTLModel 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 Lm46;
for s being set st s in S holds
(Fid f,S) . s = (Fid (Tau (SIGMA f),R,BASSIGN),S) . s

proof

let s be set ; :: 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 Lm48, FUNCT_2:18; :: thesis: verum