let I be set ; :: thesis: for A being V8() ManySortedSet of I
for F being ManySortedFunction of A, [[0]] I holds F = [[0]] I
let A be V8() ManySortedSet of I; :: 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