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