let S be non empty finite set ; :: thesis: for s being FinSequence of S
for A being Subset of (dom s)
for f being Function st f = canFS A holds
(extract (s,A)) * (f ") = s | A
let s be FinSequence of S; :: thesis: for A being Subset of (dom s)
for f being Function st f = canFS A holds
(extract (s,A)) * (f ") = s | A
let A be Subset of (dom s); :: thesis: for f being Function st f = canFS A holds
(extract (s,A)) * (f ") = s | A
let f be Function; :: thesis: ( f = canFS A implies (extract (s,A)) * (f ") = s | A )
assume A1: f = canFS A ; :: thesis: (extract (s,A)) * (f ") = s | A
A2: f * (f ") = id (rng f) by A1, FUNCT_1:39
.= id A by A1, FUNCT_2:def 3 ;
A3: dom (s | A) = (dom s) /\ A by RELAT_1:61
.= dom (s * (id A)) by FUNCT_1:19 ;

now :: thesis: for x being object st x in dom (s | A) holds
(s | A) . x = (s * (id A)) . x

let x be object ; :: thesis: ( x in dom (s | A) implies (s | A) . x = (s * (id A)) . x )
assume A4: x in dom (s | A) ; :: thesis: (s | A) . x = (s * (id A)) . x
then A5: x in (dom s) /\ A by RELAT_1:61;
thus (s | A) . x = s . x by A4, FUNCT_1:47
.= (s * (id A)) . x by A5, FUNCT_1:20 ; :: thesis: verum

end;

then A6: s * (id A) = s | A by A3, FUNCT_1:2;
thus (extract (s,A)) * (f ") = s | A by A6, A2, A1, RELAT_1:36; :: thesis: verum