deffunc H₁( set ) -> set = (chi T,S) . $1;
A1: for x being set st x in S holds
H₁(x) in BOOLEAN

proof

let x be set ; :: thesis: ( x in S implies H₁(x) in BOOLEAN )
assume A2: x in S ; :: thesis: H₁(x) in BOOLEAN

per cases ( x in T or not x in T ) ;

suppose x in T ; :: thesis: H₁(x) in BOOLEAN

then H₁(x) = 1 by FUNCT_3:def 3;
hence H₁(x) in BOOLEAN by TARSKI:def 2; :: thesis: verum

end;

suppose not x in T ; :: thesis: H₁(x) in BOOLEAN

then H₁(x) = 0 by A2, FUNCT_3:def 3;
hence H₁(x) in BOOLEAN by TARSKI:def 2; :: thesis: verum

end;

end;

end;

consider IT being Function of S,BOOLEAN such that
A3: for x being set st x in S holds
IT . x = H₁(x) from FUNCT_2:sch 2(A1);
reconsider IT = IT as Assign of (BASSModel R,BASSIGN) by FUNCT_2:11;
take IT ; :: thesis: for s being set st s in S holds
(Fid IT,S) . s = (chi T,S) . s
Fid IT,S = IT by Def41;
hence for s being set st s in S holds
(Fid IT,S) . s = (chi T,S) . s by A3; :: thesis: verum