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 A2: s in S ; :: thesis: (Fid f,S) . s = (Fid (Tau (SIGMA f),R,BASSIGN),S) . s
reconsider s = s as Element of S by A2;

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

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

then consider x being Element of S such that
A4: x = s and
A5: (Fid f,S) . x = TRUE by A1;
(Fid (Tau (SIGMA f),R,BASSIGN),S) . s = (chi (SIGMA f),S) . s by Def64
.= 1 by A3, FUNCT_3:def 3 ;
hence (Fid f,S) . s = (Fid (Tau (SIGMA f),R,BASSIGN),S) . s by A4, A5; :: thesis: verum

end;

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

A7: (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, A6; :: thesis: verum

end;

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

end;

end;

end;

then Fid f,S = Fid (Tau (SIGMA f),R,BASSIGN),S by FUNCT_2:18;
hence Tau (SIGMA f),R,BASSIGN = f by Lm48; :: thesis: verum