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