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

proof

let x be object ; :: 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 object 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:8;
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