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 & 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 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 Nat st d1 is_common_for_dom f & n <> 0 holds
d1 is_common_for_dom f | n
let n be Nat; :: thesis: ( d1 is_common_for_dom f & n <> 0 implies d1 is_common_for_dom f | n )
assume that
A1: d1 is_common_for_dom f and
A2: n <> 0 ; :: 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) )
assume A3: m in dom (f | n) ; :: thesis: d1 in dom ((f | n) . m)
set G = (f | n) . m;

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

suppose n >= len f ; :: thesis: d1 in dom ((f | n) . m)

then f | n = f by Lm1;
hence d1 in dom ((f | n) . m) by A1, A3; :: thesis: verum

end;

suppose A4: n < len f ; :: thesis: d1 in dom ((f | n) . m)

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

end;

end;