let i, I be set ; :: thesis: for M being ManySortedSet of I
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 I; :: 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)}
( dom |:SF:| = I & |:SF:| = |.SF.| ) by A2, Def3, PARTFUN1:def 2;
hence |:SF:| . i = {(f . i),(f1 . i)} by A1, A2, Th19; :: thesis: verum