deffunc H1( object ) -> set = (chi (T,S)) . $1;
A1: for x being object st x in S holds
H1(x) in BOOLEAN
proof
let x be object ; :: thesis: ( x in S implies H1(x) in BOOLEAN )
assume A2: x in S ; :: thesis: H1(x) in BOOLEAN
per cases ( x in T or not x in T ) ;
end;
end;
consider IT being Function of S,BOOLEAN such that
A3: for x being object st x in S holds
IT . x = H1(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