let I be set ; :: thesis: for f being non-empty ManySortedSet of I
for p being I -defined b₁ -compatible Function ex s being b₁ -compatible ManySortedSet of I st p c= s
let f be non-empty ManySortedSet of I; :: thesis: for p being I -defined f -compatible Function ex s being f -compatible ManySortedSet of I st p c= s
let p be I -defined f -compatible Function; :: thesis: ex s being f -compatible ManySortedSet of I st p c= s
set h = the f -compatible ManySortedSet of I;
take the f -compatible ManySortedSet of I +* p ; :: thesis: p c= the f -compatible ManySortedSet of I +* p
thus p c= the f -compatible ManySortedSet of I +* p by FUNCT_4:25; :: thesis: verum