let cF1, cF2 be complex-valued XFinSequence; :: thesis: for c being Complex holds c + (cF1 ^ cF2) = (c + cF1) ^ (c + cF2)
let c be Complex; :: thesis: c + (cF1 ^ cF2) = (c + cF1) ^ (c + cF2)
A1: ( dom (c + cF1) = dom cF1 & dom (c + cF2) = dom cF2 & dom (c + (cF1 ^ cF2)) = dom (cF1 ^ cF2) ) by VALUED_1:def 2;
A2: ( len (cF1 ^ cF2) = (len cF1) + (len cF2) & len ((c + cF1) ^ (c + cF2)) = (len (c + cF1)) + (len (c + cF2)) ) by AFINSQ_1:17;
for x being object st x in dom (c + (cF1 ^ cF2)) holds
(c + (cF1 ^ cF2)) . x = ((c + cF1) ^ (c + cF2)) . x

proof

let x be object ; :: thesis: ( x in dom (c + (cF1 ^ cF2)) implies (c + (cF1 ^ cF2)) . x = ((c + cF1) ^ (c + cF2)) . x )
assume A3: x in dom (c + (cF1 ^ cF2)) ; :: thesis: (c + (cF1 ^ cF2)) . x = ((c + cF1) ^ (c + cF2)) . x
then reconsider i = x as Nat ;

per cases ( i in dom cF1 or ex n being Nat st
( n in dom cF2 & i = (len cF1) + n ) ) by A3, A1, AFINSQ_1:20;

suppose A4: i in dom cF1 ; :: thesis: (c + (cF1 ^ cF2)) . x = ((c + cF1) ^ (c + cF2)) . x

then A5: ( (cF1 ^ cF2) . i = cF1 . i & ((c + cF1) ^ (c + cF2)) . i = (c + cF1) . i ) by A1, AFINSQ_1:def 3;
hence (c + (cF1 ^ cF2)) . x = c + (cF1 . i) by A3, VALUED_1:def 2
.= ((c + cF1) ^ (c + cF2)) . x by A5, A4, A1, VALUED_1:def 2 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom cF2 & i = (len cF1) + n ) ; :: thesis: (c + (cF1 ^ cF2)) . x = ((c + cF1) ^ (c + cF2)) . x

then consider n being Nat such that
A6: ( n in dom cF2 & i = (len cF1) + n ) ;
A7: ( (cF1 ^ cF2) . i = cF2 . n & ((c + cF1) ^ (c + cF2)) . i = (c + cF2) . n ) by A1, A6, AFINSQ_1:def 3;
hence (c + (cF1 ^ cF2)) . x = c + (cF2 . n) by A3, VALUED_1:def 2
.= ((c + cF1) ^ (c + cF2)) . x by A1, A6, A7, VALUED_1:def 2 ;
:: thesis: verum

end;

end;

end;

hence c + (cF1 ^ cF2) = (c + cF1) ^ (c + cF2) by A1, A2, FUNCT_1:2; :: thesis: verum