let G1, G2 be non empty non void Circuit-like ManySortedSign ; :: thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for s being State of C2 holds s * f is State of C1
let f, g be Function; :: thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for s being State of C2 holds s * f is State of C1
let C1 be non-empty Circuit of G1; :: thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for s being State of C2 holds s * f is State of C1
let C2 be non-empty Circuit of G2; :: thesis: ( f,g form_embedding_of C1,C2 implies for s being State of C2 holds s * f is State of C1 )
set S1 = G1;
set S2 = G2;
assume that
f is one-to-one and
g is one-to-one and
A1: f,g form_morphism_between G1,G2 and
A2: the Sorts of C1 = the Sorts of C2 * f and
the Charact of C1 = the Charact of C2 * g ; :: according to CIRCTRM1:def 12 :: thesis: for s being State of C2 holds s * f is State of C1
let s be State of C2; :: thesis: s * f is State of C1
A3: dom the Sorts of C2 = the carrier of G2 by PARTFUN1:def 2;
A4: dom the Sorts of C1 = the carrier of G1 by PARTFUN1:def 2;
A5: dom s = dom the Sorts of C2 by CARD_3:9;
A6: rng f c= the carrier of G2 by A1;
A7: dom f = the carrier of G1 by A1;
then A8: dom (s * f) = the carrier of G1 by A3, A5, A6, RELAT_1:27;

now :: thesis: for x being object st x in the carrier of G1 holds
(s * f) . x in the Sorts of C1 . x

let x be object ; :: thesis: ( x in the carrier of G1 implies (s * f) . x in the Sorts of C1 . x )
assume A9: x in the carrier of G1 ; :: thesis: (s * f) . x in the Sorts of C1 . x
then A10: f . x in rng f by A7, FUNCT_1:def 3;
(s * f) . x = s . (f . x) by A7, A9, FUNCT_1:13;
then (s * f) . x in the Sorts of C2 . (f . x) by A3, A6, A10, CARD_3:9;
hence (s * f) . x in the Sorts of C1 . x by A2, A7, A9, FUNCT_1:13; :: thesis: verum

end;

hence s * f is State of C1 by A4, A8, CARD_3:9; :: thesis: verum