let X be set ; :: thesis: for W being non empty set

for h being PartFunc of W,REAL

for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds

((h ^) | X) /* seq = ((h | X) /* seq) "

let W be non empty set ; :: thesis: for h being PartFunc of W,REAL

for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds

((h ^) | X) /* seq = ((h | X) /* seq) "

let h be PartFunc of W,REAL; :: thesis: for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds

((h ^) | X) /* seq = ((h | X) /* seq) "

let seq be sequence of W; :: 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) "

for h being PartFunc of W,REAL

for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds

((h ^) | X) /* seq = ((h | X) /* seq) "

let W be non empty set ; :: thesis: for h being PartFunc of W,REAL

for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds

((h ^) | X) /* seq = ((h | X) /* seq) "

let h be PartFunc of W,REAL; :: thesis: for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds

((h ^) | X) /* seq = ((h | X) /* seq) "

let seq be sequence of W; :: 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)

then A5:
rng seq c= dom ((h ^) | X)
by TARSKI:def 3;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 " {0}) by A2, XBOOLE_0:def 4;

then A4: x in dom (h ^) by RFUNCT_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;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 " {0}) by A2, XBOOLE_0:def 4;

then A4: x in dom (h ^) by RFUNCT_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

now :: thesis: for n being Element of NAT holds (((h ^) | X) /* seq) . n = (((h | X) /* seq) ") . n

hence
((h ^) | X) /* seq = ((h | X) /* seq) "
by FUNCT_2:63; :: thesis: verumlet 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 A8: seq . n in X by XBOOLE_0:def 4;

seq . n in (dom h) \ (h " {0}) by A2, A7, XBOOLE_0:def 4;

then A9: seq . n in dom (h ^) by RFUNCT_1:def 2;

thus (((h ^) | X) /* seq) . n = ((h ^) | X) . (seq . n) by A5, FUNCT_2:108

.= (h ^) . (seq . n) by A8, FUNCT_1:49

.= (h . (seq . n)) " by A9, RFUNCT_1:def 2

.= ((h | X) . (seq . n)) " by A1, A6, FUNCT_1:47

.= (((h | X) /* seq) . n) " by A1, FUNCT_2:108

.= (((h | X) /* seq) ") . n by VALUED_1:10 ; :: thesis: verum

end;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 A8: seq . n in X by XBOOLE_0:def 4;

seq . n in (dom h) \ (h " {0}) by A2, A7, XBOOLE_0:def 4;

then A9: seq . n in dom (h ^) by RFUNCT_1:def 2;

thus (((h ^) | X) /* seq) . n = ((h ^) | X) . (seq . n) by A5, FUNCT_2:108

.= (h ^) . (seq . n) by A8, FUNCT_1:49

.= (h . (seq . n)) " by A9, RFUNCT_1:def 2

.= ((h | X) . (seq . n)) " by A1, A6, FUNCT_1:47

.= (((h | X) /* seq) . n) " by A1, FUNCT_2:108

.= (((h | X) /* seq) ") . n by VALUED_1:10 ; :: thesis: verum