let a be object ; :: thesis: for R being Relation st R is well-ordering holds

field (R |_2 (R -Seg a)) = R -Seg a

let R be Relation; :: thesis: ( R is well-ordering implies field (R |_2 (R -Seg a)) = R -Seg a )

R -Seg a c= field R by Th9;

hence ( R is well-ordering implies field (R |_2 (R -Seg a)) = R -Seg a ) by Th31; :: thesis: verum

field (R |_2 (R -Seg a)) = R -Seg a

let R be Relation; :: thesis: ( R is well-ordering implies field (R |_2 (R -Seg a)) = R -Seg a )

R -Seg a c= field R by Th9;

hence ( R is well-ordering implies field (R |_2 (R -Seg a)) = R -Seg a ) by Th31; :: thesis: verum