let f, g, h, 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 ;
len (f ^ g) = (len h) + (len k) by ;
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 ;
then len ((f - h) ^ (g - k)) = (len f) + (len g) by ;
then len ((f ^ g) - (h ^ k)) = len ((f - h) ^ (g - k)) by ;
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 ;
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 ;
A10: dom f = dom (f - h) by ;
A11: dom h = dom (f - h) by ;
((f ^ g) - (h ^ k)) . d = ((f ^ g) . d) - ((h ^ k) . d) by
.= (f . d) - ((h ^ k) . d) by
.= (f . d) - (h . d) by ;
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 ;
then A14: (f ^ g) . d = g . e by ;
e in dom k by ;
then A15: (h ^ k) . d = k . e by ;
((f - h) ^ (g - k)) . d = (g - k) . e by
.= (g . e) - (k . e) by ;
hence ((f - h) ^ (g - k)) . d = ((f ^ g) - (h ^ k)) . d by ; :: thesis: verum
end;
end;
end;
hence (f ^ g) - (h ^ k) = (f - h) ^ (g - k) by A6; :: thesis: verum