let D1, D2 be non empty set ; :: thesis: for p being FinSequence of D1
for f being Function of D1,D2 holds
( dom (f * p) = dom p & len (f * p) = len p & ( for n being Nat st n in dom (f * p) holds
(f * p) . n = f . (p . n) ) )
let p be FinSequence of D1; :: thesis: for f being Function of D1,D2 holds
( dom (f * p) = dom p & len (f * p) = len p & ( for n being Nat st n in dom (f * p) holds
(f * p) . n = f . (p . n) ) )
let f be Function of D1,D2; :: thesis: ( dom (f * p) = dom p & len (f * p) = len p & ( for n being Nat st n in dom (f * p) holds
(f * p) . n = f . (p . n) ) )
A1: ( rng p c= D1 & dom f = D1 ) by FUNCT_2:def 1;
hence dom (f * p) = dom p by RELAT_1:27; :: thesis: ( len (f * p) = len p & ( for n being Nat st n in dom (f * p) holds
(f * p) . n = f . (p . n) ) )
dom (f * p) = dom p by A1, RELAT_1:27;
hence len (f * p) = len p by Th27; :: thesis: for n being Nat st n in dom (f * p) holds
(f * p) . n = f . (p . n)
let n be Nat; :: thesis: ( n in dom (f * p) implies (f * p) . n = f . (p . n) )
assume n in dom (f * p) ; :: thesis: (f * p) . n = f . (p . n)
hence (f * p) . n = f . (p . n) by FUNCT_1:12; :: thesis: verum