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