let I be non empty set ; :: thesis: for X being disjoint_valued ManySortedSet of I
for D being V2() ManySortedSet of I
for F1, F2 being ManySortedFunction of X,D st Flatten F1 = Flatten F2 holds
F1 = F2
let X be disjoint_valued ManySortedSet of I; :: thesis: for D being V2() ManySortedSet of I
for F1, F2 being ManySortedFunction of X,D st Flatten F1 = Flatten F2 holds
F1 = F2
let D be V2() ManySortedSet of I; :: thesis: for F1, F2 being ManySortedFunction of X,D st Flatten F1 = Flatten F2 holds
F1 = F2
let F1, F2 be ManySortedFunction of X,D; :: thesis: ( Flatten F1 = Flatten F2 implies F1 = F2 )
assume A1: Flatten F1 = Flatten F2 ; :: thesis: F1 = F2
now :: thesis: for i being object st i in I holds
F1 . i = F2 . i
let i be object ; :: thesis: ( i in I implies F1 . i = F2 . i )
assume A2: i in I ; :: thesis: F1 . i = F2 . i
then reconsider Di = D . i as non empty set ;
reconsider f1 = F1 . i, f2 = F2 . i as Function of (X . i),Di by A2, PBOOLE:def 15;
now :: thesis: for x being object st x in X . i holds
f1 . x = f2 . x
let x be object ; :: thesis: ( x in X . i implies f1 . x = f2 . x )
assume A3: x in X . i ; :: thesis: f1 . x = f2 . x
hence f1 . x = (Flatten F1) . x by A2, Def1
.= f2 . x by A1, A2, A3, Def1 ;
:: thesis: verum
end;
hence F1 . i = F2 . i by FUNCT_2:12; :: thesis: verum
end;
hence F1 = F2 ; :: thesis: verum