let p, q be PartialPredicate of F_{1}(); :: thesis: ( dom p = F_{2}() & ( for d being object st d in dom p holds

( ( P_{1}[d] implies p . d = TRUE ) & ( P_{1}[d] implies p . d = FALSE ) ) ) & dom q = F_{2}() & ( for d being object st d in dom q holds

( ( P_{1}[d] implies q . d = TRUE ) & ( P_{1}[d] implies q . d = FALSE ) ) ) implies p = q )

assume that

A1: ( dom p = F_{2}() & ( for d being object st d in dom p holds

( ( P_{1}[d] implies p . d = TRUE ) & ( P_{1}[d] implies p . d = FALSE ) ) ) )
and

A2: ( dom q = F_{2}() & ( for d being object st d in dom q holds

( ( P_{1}[d] implies q . d = TRUE ) & ( P_{1}[d] implies q . d = FALSE ) ) ) )
; :: thesis: p = q

for d being object st d in dom p holds

p . d = q . d

( ( P

( ( P

assume that

A1: ( dom p = F

( ( P

A2: ( dom q = F

( ( P

for d being object st d in dom p holds

p . d = q . d

proof

hence
p = q
by A1, A2, FUNCT_1:2; :: thesis: verum
let d be object ; :: thesis: ( d in dom p implies p . d = q . d )

assume A3: d in dom p ; :: thesis: p . d = q . d

p . d = q . d hence p . d = q . d ; :: thesis: verum

end;assume A3: d in dom p ; :: thesis: p . d = q . d

p . d = q . d hence p . d = q . d ; :: thesis: verum