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 that
A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) and
A2: f = g and
A3: ( f is idempotent & f is monotone ) ; :: according to WAYBEL_1:def 13 :: thesis: g is projection
thus ( g is idempotent & g is monotone ) by A1, A2, A3, WAYBEL_9:1; :: according to WAYBEL_1:def 13 :: thesis: verum