reconsider D = the carrier of (QuotientOrder A) as a_partition of the carrier of A by Th47;

reconsider Y = X as Element of D ;

take eqSupport (f,Y) ; :: thesis: ex D being a_partition of the carrier of A ex Y being Element of D st

( D = the carrier of (QuotientOrder A) & Y = X & eqSupport (f,Y) = eqSupport (f,Y) )

take D ; :: thesis: ex Y being Element of D st

( D = the carrier of (QuotientOrder A) & Y = X & eqSupport (f,Y) = eqSupport (f,Y) )

take Y ; :: thesis: ( D = the carrier of (QuotientOrder A) & Y = X & eqSupport (f,Y) = eqSupport (f,Y) )

thus ( D = the carrier of (QuotientOrder A) & Y = X & eqSupport (f,Y) = eqSupport (f,Y) ) ; :: thesis: verum

reconsider Y = X as Element of D ;

take eqSupport (f,Y) ; :: thesis: ex D being a_partition of the carrier of A ex Y being Element of D st

( D = the carrier of (QuotientOrder A) & Y = X & eqSupport (f,Y) = eqSupport (f,Y) )

take D ; :: thesis: ex Y being Element of D st

( D = the carrier of (QuotientOrder A) & Y = X & eqSupport (f,Y) = eqSupport (f,Y) )

take Y ; :: thesis: ( D = the carrier of (QuotientOrder A) & Y = X & eqSupport (f,Y) = eqSupport (f,Y) )

thus ( D = the carrier of (QuotientOrder A) & Y = X & eqSupport (f,Y) = eqSupport (f,Y) ) ; :: thesis: verum