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