let Omega be non empty set ; :: thesis: Omega --> 1 = chi (Omega,Omega)
set E0 = Omega --> 1;
A1: dom (chi (Omega,Omega)) = Omega by FUNCT_3:def 3;
A2: dom (Omega --> 1) = Omega by FUNCT_2:def 1;

now :: thesis: for x being object st x in dom (chi (Omega,Omega)) holds
(chi (Omega,Omega)) . x = (Omega --> 1) . x

let x be object ; :: thesis: ( x in dom (chi (Omega,Omega)) implies (chi (Omega,Omega)) . b₁ = (Omega --> 1) . b₁ )
assume A3: x in dom (chi (Omega,Omega)) ; :: thesis: (chi (Omega,Omega)) . b₁ = (Omega --> 1) . b₁

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

suppose x in Omega ; :: thesis: (chi (Omega,Omega)) . b₁ = (Omega --> 1) . b₁

hence (chi (Omega,Omega)) . x = 1 by FUNCT_3:def 3
.= (Omega --> 1) . x by A3, FUNCOP_1:7 ;
:: thesis: verum

end;

suppose not x in Omega ; :: thesis: (chi (Omega,Omega)) . b₁ = (Omega --> 1) . b₁

hence (chi (Omega,Omega)) . x = (Omega --> 1) . x by A3; :: thesis: verum

end;

end;

end;

hence Omega --> 1 = chi (Omega,Omega) by A1, A2, FUNCT_1:2; :: thesis: verum