let X, Y be set ; :: thesis: ( Y c= X implies chi (X,Y) = chi (Y,Y) )
assume A1: Y c= X ; :: thesis: chi (X,Y) = chi (Y,Y)

now :: thesis: ( dom (chi (X,Y)) = dom (chi (Y,Y)) & ( for x being object st x in dom (chi (X,Y)) holds
(chi (X,Y)) . x = (chi (Y,Y)) . x ) )

thus dom (chi (X,Y)) = Y by FUNCT_3:def 3
.= dom (chi (Y,Y)) by FUNCT_3:def 3 ; :: thesis: for x being object st x in dom (chi (X,Y)) holds
(chi (X,Y)) . x = (chi (Y,Y)) . x

hereby :: thesis: verum

let x be object ; :: thesis: ( x in dom (chi (X,Y)) implies (chi (X,Y)) . x = (chi (Y,Y)) . x )
assume A2: x in dom (chi (X,Y)) ; :: thesis: (chi (X,Y)) . x = (chi (Y,Y)) . x
then ( x in Y & x in X ) by A1;
hence (chi (X,Y)) . x = 1 by FUNCT_3:def 3
.= (chi (Y,Y)) . x by A2, FUNCT_3:def 3 ;
:: thesis: verum

end;

end;

hence chi (X,Y) = chi (Y,Y) ; :: thesis: verum