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:167;
consider n being Nat such that
A3: P c= Seg n by Th43;
A4: rng (Sgm P) = P by A3, FINSEQ_1:def 13;
A5: n in NAT by ORDINAL1:def 13;
rng ((Sgm P) | ((Sgm P) " X)) = (Sgm P) .: ((Sgm P) " X) by RELAT_1:148
.= X by A1, A4, FUNCT_1:147 ;
hence Sgm X = (Sgm P) * (Sgm ((Sgm P) " X)) by A3, A5, A2, GRAPH_2:3; :: thesis: verum