let n be Nat; :: thesis: for U1 being non empty partial non-empty UAStr st n in dom the charact of U1 holds
the charact of U1 . n is PartFunc of ( the carrier of U1 *), the carrier of U1
let U1 be non empty partial non-empty UAStr ; :: thesis: ( n in dom the charact of U1 implies the charact of U1 . n is PartFunc of ( the carrier of U1 *), the carrier of U1 )
set o = the charact of U1;
assume n in dom the charact of U1 ; :: thesis: the charact of U1 . n is PartFunc of ( the carrier of U1 *), the carrier of U1
then A1: the charact of U1 . n in rng the charact of U1 by FUNCT_1:def 5;
rng the charact of U1 c= PFuncs (( the carrier of U1 *), the carrier of U1) by FINSEQ_1:def 4;
hence the charact of U1 . n is PartFunc of ( the carrier of U1 *), the carrier of U1 by A1, PARTFUN1:121; :: thesis: verum