let D1, D2 be non empty set ; :: thesis: for f being FinSequence of PFuncs (D1,D2)
for d being Element of D1
for n being Nat st d is_common_for_dom f holds
d is_common_for_dom f /^ n
let f be FinSequence of PFuncs (D1,D2); :: thesis: for d being Element of D1
for n being Nat st d is_common_for_dom f holds
d is_common_for_dom f /^ n
let d1 be Element of D1; :: thesis: for n being Nat st d1 is_common_for_dom f holds
d1 is_common_for_dom f /^ n
let n be Nat; :: thesis: ( d1 is_common_for_dom f implies d1 is_common_for_dom f /^ n )
assume A1: d1 is_common_for_dom f ; :: thesis: d1 is_common_for_dom f /^ n
let m be Nat; :: according to RFUNCT_3:def 9 :: thesis: ( m in dom (f /^ n) implies d1 in dom ((f /^ n) . m) )
set fn = f /^ n;
assume A2: m in dom (f /^ n) ; :: thesis: d1 in dom ((f /^ n) . m)
set G = (f /^ n) . m;
now :: thesis: ( ( len f < n & d1 in dom ((f /^ n) . m) ) or ( n <= len f & d1 in dom ((f /^ n) . m) ) )
per cases ( len f < n or n <= len f ) ;
case len f < n ; :: thesis: d1 in dom ((f /^ n) . m)
hence d1 in dom ((f /^ n) . m) by A2, RELAT_1:38, RFINSEQ:def 1; :: thesis: verum
end;
case A3: n <= len f ; :: thesis: d1 in dom ((f /^ n) . m)
( 1 <= m & m <= m + n ) by A2, FINSEQ_3:25, NAT_1:11;
then A4: 1 <= m + n by XXREAL_0:2;
A5: m <= len (f /^ n) by A2, FINSEQ_3:25;
len (f /^ n) = (len f) - n by A3, RFINSEQ:def 1;
then m + n <= len f by A5, XREAL_1:19;
then A6: m + n in dom f by A4, FINSEQ_3:25;
(f /^ n) . m = f . (m + n) by A2, A3, RFINSEQ:def 1;
hence d1 in dom ((f /^ n) . m) by A1, A6; :: thesis: verum
end;
end;
end;
hence d1 in dom ((f /^ n) . m) ; :: thesis: verum