let i, I be set ; 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; 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; 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; ( i in I & SF = {f,f1} implies |:SF:| . i = {(f . i),(f1 . i)} )
assume that
A1:
i in I
and
A2:
SF = {f,f1}
; |: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; verum