let X be set ; :: thesis: for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h | X) & h " {0} = {} holds
((h ^) | X) /* seq = ((h | X) /* seq) "
let seq be Complex_Sequence; :: thesis: for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h | X) & h " {0} = {} holds
((h ^) | X) /* seq = ((h | X) /* seq) "
let h be PartFunc of COMPLEX,COMPLEX; :: thesis: ( rng seq c= dom (h | X) & h " {0} = {} implies ((h ^) | X) /* seq = ((h | X) /* seq) " )
assume that
A1: rng seq c= dom (h | X) and
A2: h " {0} = {} ; :: thesis: ((h ^) | X) /* seq = ((h | X) /* seq) "
now :: thesis: for x being object st x in rng seq holds
x in dom ((h ^) | X)
let x be object ; :: thesis: ( x in rng seq implies x in dom ((h ^) | X) )
assume x in rng seq ; :: thesis: x in dom ((h ^) | X)
then x in dom (h | X) by A1;
then A3: x in (dom h) /\ X by RELAT_1:61;
then x in (dom h) \ (h " {0c}) by A2, XBOOLE_0:def 4;
then A4: x in dom (h ^) by CFUNCT_1:def 2;
x in X by A3, XBOOLE_0:def 4;
then x in (dom (h ^)) /\ X by A4, XBOOLE_0:def 4;
hence x in dom ((h ^) | X) by RELAT_1:61; :: thesis: verum
end;
then A5: rng seq c= dom ((h ^) | X) ;
now :: thesis: for n being Element of NAT holds (((h ^) | X) /* seq) . n = (((h | X) /* seq) ") . n
let n be Element of NAT ; :: thesis: (((h ^) | X) /* seq) . n = (((h | X) /* seq) ") . n
A6: seq . n in rng seq by VALUED_0:28;
then seq . n in dom (h | X) by A1;
then A7: seq . n in (dom h) /\ X by RELAT_1:61;
then seq . n in (dom h) \ (h " {0c}) by A2, XBOOLE_0:def 4;
then A8: seq . n in dom (h ^) by CFUNCT_1:def 2;
seq . n in X by A7, XBOOLE_0:def 4;
then seq . n in (dom (h ^)) /\ X by A8, XBOOLE_0:def 4;
then A9: seq . n in dom ((h ^) | X) by RELAT_1:61;
thus (((h ^) | X) /* seq) . n = ((h ^) | X) /. (seq . n) by A5, FUNCT_2:109
.= (h ^) /. (seq . n) by A9, PARTFUN2:15
.= (h /. (seq . n)) " by A8, CFUNCT_1:def 2
.= ((h | X) /. (seq . n)) " by A1, A6, PARTFUN2:15
.= (((h | X) /* seq) . n) " by A1, FUNCT_2:109
.= (((h | X) /* seq) ") . n by VALUED_1:10 ; :: thesis: verum
end;
hence ((h ^) | X) /* seq = ((h | X) /* seq) " by FUNCT_2:63; :: thesis: verum