let I be set ; :: thesis: for A being V8() ManySortedSet of
for F being ManySortedFunction of A, [0] I holds F = [0] I
let A be V8() ManySortedSet of ; :: thesis: for F being ManySortedFunction of A, [0] I holds F = [0] I
let F be ManySortedFunction of A, [0] I; :: thesis: F = [0] I

now

let i be set ; :: thesis: ( i in I implies F . i = ([0] I) . i )
assume i in I ; :: thesis: F . i = ([0] I) . i
then reconsider f = F . i as Function of (A . i),(([0] I) . i) by PBOOLE:def 18;
([0] I) . i = {} by PBOOLE:5;
then f = {} ;
hence F . i = ([0] I) . i by PBOOLE:5; :: thesis: verum

end;

hence F = [0] I by PBOOLE:3; :: thesis: verum