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
A2: [x,y] in p by RELAT_1:def 5;
A3: p in {p,f} by TARSKI:def 2;
A4: {p,f} in {{p,f},{p}} by TARSKI:def 2;
A5: y in {x,y} by TARSKI:def 2;
A6: {x,y} in {{x,y},{x}} by TARSKI:def 2;
A7: the_rank_of y in the_rank_of {x,y} by A5, Th76;
A8: the_rank_of {x,y} in the_rank_of [x,y] by A6, Th76;
A9: the_rank_of p in the_rank_of {p,f} by A3, Th76;
A10: the_rank_of {p,f} in the_rank_of [p,f] by A4, Th76;
A11: the_rank_of y in the_rank_of [x,y] by A7, A8, ORDINAL1:19;
A12: the_rank_of [x,y] in the_rank_of p by A2, Th76;
A13: the_rank_of p in the_rank_of [p,f] by A9, A10, ORDINAL1:19;
the_rank_of y in the_rank_of p by A11, A12, ORDINAL1:19;
hence the_rank_of y in the_rank_of [p,f] by A13, ORDINAL1:19; :: thesis: verum