let i, I be set ; :: thesis: for M being ManySortedSet of I
for f being Function
for SF being SubsetFamily of M st i in I & SF = {f} holds
|:SF:| . i = {(f . i)}
let M be ManySortedSet of I; :: thesis: for f being Function
for SF being SubsetFamily of M st i in I & SF = {f} holds
|:SF:| . i = {(f . i)}
let f be Function; :: thesis: for SF being SubsetFamily of M st i in I & SF = {f} holds
|:SF:| . i = {(f . i)}
let SF be SubsetFamily of M; :: thesis: ( i in I & SF = {f} implies |:SF:| . i = {(f . i)} )
assume that
A1: i in I and
A2: SF = {f} ; :: thesis: |:SF:| . i = {(f . i)}
A3: |:SF:| = |.SF.| by A2, Def3;
dom |:SF:| = I by PARTFUN1:def 2;
then i in dom f by A1, A2, A3, Th15;
hence |:SF:| . i = {(f . i)} by A2, A3, Th17; :: thesis: verum