let f, h, g, k be FinSequence of REAL ; :: thesis: ( len f = len h & len g = len k implies (f ^ g) - (h ^ k) = (f - h) ^ (g - k) )
assume that
A1: len f = len h and
A2: len g = len k ; :: thesis: (f ^ g) - (h ^ k) = (f - h) ^ (g - k)
A3: len (f - h) = len f by A1, TOPREAL7:7;
len (f ^ g) = (len h) + (len k) by A1, A2, FINSEQ_1:22;
then len (f ^ g) = len (h ^ k) by FINSEQ_1:22;
then A4: len ((f ^ g) - (h ^ k)) = len (f ^ g) by TOPREAL7:7;
A5: len (g - k) = len g by A2, TOPREAL7:7;
then len ((f - h) ^ (g - k)) = (len f) + (len g) by A3, FINSEQ_1:22;
then len ((f ^ g) - (h ^ k)) = len ((f - h) ^ (g - k)) by A4, FINSEQ_1:22;
then A6: dom ((f ^ g) - (h ^ k)) = dom ((f - h) ^ (g - k)) by FINSEQ_3:29;
for d being Nat st d in dom ((f - h) ^ (g - k)) holds
((f - h) ^ (g - k)) . d = ((f ^ g) - (h ^ k)) . d

proof

let d be Nat; :: thesis: ( d in dom ((f - h) ^ (g - k)) implies ((f - h) ^ (g - k)) . d = ((f ^ g) - (h ^ k)) . d )
assume A7: d in dom ((f - h) ^ (g - k)) ; :: thesis: ((f - h) ^ (g - k)) . d = ((f ^ g) - (h ^ k)) . d

per cases ( d in dom (f - h) or ex e being Nat st
( e in dom (g - k) & d = (len (f - h)) + e ) ) by A7, FINSEQ_1:25;

suppose A8: d in dom (f - h) ; :: thesis: ((f - h) ^ (g - k)) . d = ((f ^ g) - (h ^ k)) . d

then A9: ((f - h) ^ (g - k)) . d = (f - h) . d by FINSEQ_1:def 7
.= (f . d) - (h . d) by A8, VALUED_1:13 ;
A10: dom f = dom (f - h) by A1, TOPREAL7:7;
A11: dom h = dom (f - h) by A1, A3, FINSEQ_3:29;
((f ^ g) - (h ^ k)) . d = ((f ^ g) . d) - ((h ^ k) . d) by A6, A8, FINSEQ_2:15, VALUED_1:13
.= (f . d) - ((h ^ k) . d) by A8, A10, FINSEQ_1:def 7
.= (f . d) - (h . d) by A8, A11, FINSEQ_1:def 7 ;
hence ((f - h) ^ (g - k)) . d = ((f ^ g) - (h ^ k)) . d by A9; :: thesis: verum

end;

suppose ex e being Nat st
( e in dom (g - k) & d = (len (f - h)) + e ) ; :: thesis: ((f - h) ^ (g - k)) . d = ((f ^ g) - (h ^ k)) . d

then consider e being Nat such that
A12: e in dom (g - k) and
A13: d = (len (f - h)) + e ;
e in dom g by A2, A12, TOPREAL7:7;
then A14: (f ^ g) . d = g . e by A3, A13, FINSEQ_1:def 7;
e in dom k by A2, A5, A12, FINSEQ_3:29;
then A15: (h ^ k) . d = k . e by A1, A3, A13, FINSEQ_1:def 7;
((f - h) ^ (g - k)) . d = (g - k) . e by A12, A13, FINSEQ_1:def 7
.= (g . e) - (k . e) by A12, VALUED_1:13 ;
hence ((f - h) ^ (g - k)) . d = ((f ^ g) - (h ^ k)) . d by A6, A12, A13, A14, A15, FINSEQ_1:28, VALUED_1:13; :: thesis: verum

end;

end;

end;

hence (f ^ g) - (h ^ k) = (f - h) ^ (g - k) by A6, FINSEQ_1:13; :: thesis: verum