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 & n <> 0 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 & n <> 0 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 & n <> 0 holds
d1 is_common_for_dom f | n
let n be Element of NAT ; :: thesis: ( d1 is_common_for_dom f & n <> 0 implies d1 is_common_for_dom f | n )
assume A1: ( d1 is_common_for_dom f & n <> 0 ) ; :: thesis: d1 is_common_for_dom 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 ( n >= len f or n < len f ) ;

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

then f | n = f by Lm1;
hence d1 in dom G by A1, A2, Def9; :: thesis: verum

end;

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

then A4: ( dom f = Seg (len f) & dom (f | n) = Seg (len (f | n)) & len (f | n) = n ) by FINSEQ_1:80, FINSEQ_1:def 3;
0 < n by A1;
then 0 + 1 <= n by NAT_1:13;
then n in dom f by A3, FINSEQ_3:27;
then ( G = f . m & m in dom f ) by A2, A4, RFINSEQ:19;
hence d1 in dom G by A1, Def9; :: thesis: verum

end;

end;

end;

hence d1 in dom G ; :: thesis: verum