let Y be non empty set ; :: thesis: for a being constant Function of Y,BOOLEAN holds
( a = O_el Y or a = I_el Y )
let a be constant Function of Y,BOOLEAN; :: thesis: ( a = O_el Y or a = I_el Y )
A1: ( ex n1, n2 being set st
( n1 in Y & n2 in Y & not a . n1 = a . n2 ) or for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE )
proof
assume A2: for n1, n2 being set st n1 in Y & n2 in Y holds
a . n1 = a . n2 ; :: thesis: ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE )
now :: thesis: ( not for x being Element of Y holds a . x = TRUE implies for x being Element of Y holds a . x = FALSE )
assume that
A3: not for x being Element of Y holds a . x = TRUE and
A4: not for x being Element of Y holds a . x = FALSE ; :: thesis: contradiction
consider x1 being Element of Y such that
A5: a . x1 <> TRUE by A3;
a . x1 = FALSE by A5, XBOOLEAN:def 3;
hence contradiction by A2, A4; :: thesis: verum
end;
hence ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE ) ; :: thesis: verum
end;
dom a = Y by PARTFUN1:def 2;
hence ( a = O_el Y or a = I_el Y ) by A1, Def10, Def11, FUNCT_1:def 10; :: thesis: verum