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
( dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2 )
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
( dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2 )
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
( dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2 )
let C2 be non-empty Circuit of G2; :: thesis: ( f,g form_embedding_of C1,C2 implies ( dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2 ) )
assume that
f is one-to-one and
g is one-to-one and
A1: dom f = the carrier of G1 and
A2: dom g = the carrier' of G1 and
A3: rng f c= the carrier of G2 and
A4: rng g c= the carrier' of G2 ; :: according to PUA2MSS1:def 12,CIRCTRM1:def 12 :: thesis: ( not the ResultSort of G1 * f = g * the ResultSort of G2 or ex b₁ being set ex b₂ being set st
( b₁ in the carrier' of G1 & b₂ = the Arity of G1 . b₁ & not b₂ * f = the Arity of G2 . (g . b₁) ) or not the Sorts of C1 = the Sorts of C2 * f or not the Charact of C1 = the Charact of C2 * g or ( dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2 ) )
thus ( not the ResultSort of G1 * f = g * the ResultSort of G2 or ex b₁ being set ex b₂ being set st
( b₁ in the carrier' of G1 & b₂ = the Arity of G1 . b₁ & not b₂ * f = the Arity of G2 . (g . b₁) ) or not the Sorts of C1 = the Sorts of C2 * f or not the Charact of C1 = the Charact of C2 * g or ( dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2 ) ) by A1, A2, A3, A4; :: thesis: verum