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

now

let x be set ; :: thesis: ( x in dom (chi (Omega,Omega)) implies (chi (Omega,Omega)) . b₁ = (Omega --> 1) . b₁ )
assume AS1: 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 FUNCOP_1:13, AS1 ;
:: 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 AS1; :: thesis: verum

end;

end;

end;

hence Omega --> 1 = chi (Omega,Omega) by K210, K211, FUNCT_1:9; :: thesis: verum