let S be non empty set ; 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; 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); for f being Assign of (BASSModel (R,BASSIGN)) holds Tau ((SIGMA f),R,BASSIGN) = f
let f be Assign of (BASSModel (R,BASSIGN)); 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 ;
( s in S implies (Fid (f,S)) . s = (Fid ((Tau ((SIGMA f),R,BASSIGN)),S)) . s )
assume
s in S
;
(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
;
(Fid (f,S)) . s = (Fid ((Tau ((SIGMA f),R,BASSIGN)),S)) . sA3:
(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;
verum end; suppose A4:
not
s in SIGMA f
;
(Fid (f,S)) . s = (Fid ((Tau ((SIGMA f),R,BASSIGN)),S)) . sA5:
(Fid (f,S)) . s = FALSE
(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;
verum end; end;
end;
hence
Tau ((SIGMA f),R,BASSIGN) = f
by Lm42, FUNCT_2:12; verum