let S, T be non empty RelStr ; :: thesis: for f being Function of S,S
for g being Function of T,T st RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) & f = g & f is projection holds
g is projection
let f be Function of S,S; :: thesis: for g being Function of T,T st RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) & f = g & f is projection holds
g is projection
let g be Function of T,T; :: thesis: ( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) & f = g & f is projection implies g is projection )
assume ( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) & f = g & f is idempotent & f is monotone ) ; :: according to WAYBEL_1:def 13 :: thesis: g is projection
hence ( g is idempotent & g is monotone ) by WAYBEL_9:1; :: according to WAYBEL_1:def 13 :: thesis: verum