let p, q be PartialPredicate of F1(); :: thesis: ( dom p = F2() & ( for d being object st d in dom p holds
( ( P1[d] implies p . d = TRUE ) & ( P1[d] implies p . d = FALSE ) ) ) & dom q = F2() & ( for d being object st d in dom q holds
( ( P1[d] implies q . d = TRUE ) & ( P1[d] implies q . d = FALSE ) ) ) implies p = q )
assume that
A1: ( dom p = F2() & ( for d being object st d in dom p holds
( ( P1[d] implies p . d = TRUE ) & ( P1[d] implies p . d = FALSE ) ) ) ) and
A2: ( dom q = F2() & ( for d being object st d in dom q holds
( ( P1[d] implies q . d = TRUE ) & ( P1[d] implies q . d = FALSE ) ) ) ) ; :: thesis: p = q
for d being object st d in dom p holds
p . d = q . d
proof
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
proof
per cases ( P1[d] or not P1[d] ) ;
suppose A4: P1[d] ; :: thesis: p . d = q . d
hence p . d = TRUE by A1, A3
.= q . d by A1, A2, A3, A4 ;
:: thesis: verum
end;
suppose A5: P1[d] ; :: thesis: p . d = q . d
hence p . d = FALSE by A1, A3
.= q . d by A1, A2, A3, A5 ;
:: thesis: verum
end;
end;
end;
hence p . d = q . d ; :: thesis: verum
end;
hence p = q by A1, A2, FUNCT_1:2; :: thesis: verum