per cases ( i in I or i nin dom R ) ;

suppose i in I ; :: thesis: for b₁ being Relation st b₁ = R . i holds
b₁ is strongly-normalizing

hence for b₁ being Relation st b₁ = R . i holds
b₁ is strongly-normalizing by Def16; :: thesis: verum

end;

suppose i nin dom R ; :: thesis: for b₁ being Relation st b₁ = R . i holds
b₁ is strongly-normalizing

hence for b₁ being Relation st b₁ = R . i holds
b₁ is strongly-normalizing by FUNCT_1:def 2; :: thesis: verum

end;

end;