scheme :: ABSRED_0:sch 10
isCOMP{ F1() -> non empty ARS , F2( Element of F1()) -> Element of F1() } :
F1() is COMP
provided
A1: F1() is SN and
A2: for x being Element of F1() holds x =*=> F2(x) and
A3: for x, y being Element of F1() st x <=*=> y holds
F2(x) = F2(y)