let S be non empty non void ManySortedSign ; :: thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S
set f = id the carrier of S;
set g = id the carrier' of S;
A1: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
rng the ResultSort of S c= the carrier of S ;
then (id the carrier of S) * the ResultSort of S = the ResultSort of S by RELAT_1:53;
hence ( dom (id the carrier of S) = the carrier of S & dom (id the carrier' of S) = the carrier' of S & rng (id the carrier of S) c= the carrier of S & rng (id the carrier' of S) c= the carrier' of S & (id the carrier of S) * the ResultSort of S = the ResultSort of S * (id the carrier' of S) ) by A1, RELAT_1:52; :: according to PUA2MSS1:def 12 :: thesis: for o being set
for p being Function st o in the carrier' of S & p = the Arity of S . o holds
(id the carrier of S) * p = the Arity of S . ((id the carrier' of S) . o)
let o be set ; :: thesis: for p being Function st o in the carrier' of S & p = the Arity of S . o holds
(id the carrier of S) * p = the Arity of S . ((id the carrier' of S) . o)
let p be Function; :: thesis: ( o in the carrier' of S & p = the Arity of S . o implies (id the carrier of S) * p = the Arity of S . ((id the carrier' of S) . o) )
assume that
A2: o in the carrier' of S and
A3: p = the Arity of S . o ; :: thesis: (id the carrier of S) * p = the Arity of S . ((id the carrier' of S) . o)
A4: (id the carrier' of S) . o = o by A2, FUNCT_1:17;
p in the carrier of S * by A2, A3, FUNCT_2:5;
then p is FinSequence of the carrier of S by FINSEQ_1:def 11;
then rng p c= the carrier of S by FINSEQ_1:def 4;
hence (id the carrier of S) * p = the Arity of S . ((id the carrier' of S) . o) by A3, A4, RELAT_1:53; :: thesis: verum