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