let f be set ; :: thesis: for p being Relation
for x being set st x in rng p holds
the_rank_of x in the_rank_of [p,f]
let p be Relation; :: thesis: for x being set st x in rng p holds
the_rank_of x in the_rank_of [p,f]
let y be set ; :: thesis: ( y in rng p implies the_rank_of y in the_rank_of [p,f] )
assume y in rng p ; :: thesis: the_rank_of y in the_rank_of [p,f]
then consider x being set such that
A1: [x,y] in p by RELAT_1:def 5;
( p in {p,f} & {p,f} in {{p,f},{p}} & {{p,f},{p}} = [p,f] & y in {x,y} & {x,y} in {{x,y},{x}} & {{x,y},{x}} = [x,y] ) by TARSKI:def 2;
then ( the_rank_of y in the_rank_of {x,y} & the_rank_of {x,y} in the_rank_of [x,y] & the_rank_of p in the_rank_of {p,f} & the_rank_of {p,f} in the_rank_of [p,f] ) by Th76;
then A2: ( the_rank_of y in the_rank_of [x,y] & the_rank_of [x,y] in the_rank_of p & the_rank_of p in the_rank_of [p,f] ) by A1, Th76, ORDINAL1:19;
then the_rank_of y in the_rank_of p by ORDINAL1:19;
hence the_rank_of y in the_rank_of [p,f] by A2, ORDINAL1:19; :: thesis: verum