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 Element of 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 Element of 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 Element of NAT st d1 is_common_for_dom f holds
d1 is_common_for_dom f /^ n
let n be Element of 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
set fn = f /^ n;
let G be Element of PFuncs D1,D2; :: according to RFUNCT_3:def 9 :: thesis: for n being Element of NAT st n in dom (f /^ n) & (f /^ n) . n = G holds
d1 in dom G
let m be Element of NAT ; :: thesis: ( m in dom (f /^ n) & (f /^ n) . m = G implies d1 in dom G )
assume A2: ( m in dom (f /^ n) & (f /^ n) . m = G ) ; :: thesis: d1 in dom G

now

per cases ( len f < n or n <= len f ) ;

case len f < n ; :: thesis: d1 in dom G

hence d1 in dom G by A2, RELAT_1:60, RFINSEQ:def 2; :: thesis: verum

end;

case n <= len f ; :: thesis: d1 in dom G

then A3: ( dom f = Seg (len f) & dom (f /^ n) = Seg (len (f /^ n)) & len (f /^ n) = (len f) - n & G = f . (m + n) ) by A2, FINSEQ_1:def 3, RFINSEQ:def 2;
( 1 <= m & m <= len (f /^ n) & m <= m + n ) by A2, FINSEQ_3:27, NAT_1:11;
then ( 1 <= m + n & m + n <= len f ) by A3, XREAL_1:21, XXREAL_0:2;
then m + n in dom f by FINSEQ_3:27;
hence d1 in dom G by A1, A3, Def9; :: thesis: verum

end;

end;

end;

hence d1 in dom G ; :: thesis: verum