let X be set ; :: thesis: for P being finite without_zero Subset of NAT st X c= P holds
Sgm X = (Sgm P) * (Sgm ((Sgm P) " X))
let P be finite without_zero Subset of NAT; :: thesis: ( X c= P implies Sgm X = (Sgm P) * (Sgm ((Sgm P) " X)) )
assume A1: X c= P ; :: thesis: Sgm X = (Sgm P) * (Sgm ((Sgm P) " X))
A2: (Sgm P) " X c= dom (Sgm P) by RELAT_1:132;
A3: P is included_in_Seg ;
A4: rng (Sgm P) = P by FINSEQ_1:def 14;
rng ((Sgm P) | ((Sgm P) " X)) = (Sgm P) .: ((Sgm P) " X) by RELAT_1:115
.= X by A1, A4, FUNCT_1:77 ;
hence Sgm X = (Sgm P) * (Sgm ((Sgm P) " X)) by A3, A2, FINSEQ_6:129; :: thesis: verum