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 object such that
A1: [x,y] in p by XTUPLE_0:def 13;
A2: p in {p,f} by TARSKI:def 2;
A3: {p,f} in {{p,f},{p}} by TARSKI:def 2;
A4: y in {x,y} by TARSKI:def 2;
A5: {x,y} in {{x,y},{x}} by TARSKI:def 2;
A6: the_rank_of y in the_rank_of {x,y} by A4, Th68;
A7: the_rank_of {x,y} in the_rank_of [x,y] by A5, Th68;
A8: the_rank_of p in the_rank_of {p,f} by A2, Th68;
A9: the_rank_of {p,f} in the_rank_of [p,f] by A3, Th68;
A10: the_rank_of y in the_rank_of [x,y] by A6, A7, ORDINAL1:10;
A11: the_rank_of [x,y] in the_rank_of p by A1, Th68;
A12: the_rank_of p in the_rank_of [p,f] by A8, A9, ORDINAL1:10;
the_rank_of y in the_rank_of p by A10, A11, ORDINAL1:10;
hence the_rank_of y in the_rank_of [p,f] by A12, ORDINAL1:10; :: thesis: verum