let C, D be non empty set ; :: thesis: for SC being Subset of C

for d being Element of D holds

( SC --> d is total iff SC = C )

let SC be Subset of C; :: thesis: for d being Element of D holds

( SC --> d is total iff SC = C )

let d be Element of D; :: thesis: ( SC --> d is total iff SC = C )

thus ( SC --> d is total implies SC = C ) :: thesis: ( SC = C implies SC --> d is total )

then dom (SC --> d) = C by FUNCOP_1:13;

hence SC --> d is total by PARTFUN1:def 2; :: thesis: verum

for d being Element of D holds

( SC --> d is total iff SC = C )

let SC be Subset of C; :: thesis: for d being Element of D holds

( SC --> d is total iff SC = C )

let d be Element of D; :: thesis: ( SC --> d is total iff SC = C )

thus ( SC --> d is total implies SC = C ) :: thesis: ( SC = C implies SC --> d is total )

proof

assume
SC = C
; :: thesis: SC --> d is total
assume
SC --> d is total
; :: thesis: SC = C

then dom (SC --> d) = C by PARTFUN1:def 2;

hence SC = C by FUNCOP_1:13; :: thesis: verum

end;then dom (SC --> d) = C by PARTFUN1:def 2;

hence SC = C by FUNCOP_1:13; :: thesis: verum

then dom (SC --> d) = C by FUNCOP_1:13;

hence SC --> d is total by PARTFUN1:def 2; :: thesis: verum