let CPNT1, CPNT2 be Colored-PT-net; :: thesis: for O12 being Function of (Outbds CPNT1), the carrier of CPNT2
for q12 being Function st dom q12 = Outbds CPNT1 & ( for t01 being transition of CPNT1 st t01 is outbound holds
q12 . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) ) holds
q12 in Funcs ((Outbds CPNT1),(union { (Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))))) where t01 is transition of CPNT1 : t01 is outbound } ))
let O12 be Function of (Outbds CPNT1), the carrier of CPNT2; :: thesis: for q12 being Function st dom q12 = Outbds CPNT1 & ( for t01 being transition of CPNT1 st t01 is outbound holds
q12 . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) ) holds
q12 in Funcs ((Outbds CPNT1),(union { (Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))))) where t01 is transition of CPNT1 : t01 is outbound } ))
let q12 be Function; :: thesis: ( dom q12 = Outbds CPNT1 & ( for t01 being transition of CPNT1 st t01 is outbound holds
q12 . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) ) implies q12 in Funcs ((Outbds CPNT1),(union { (Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))))) where t01 is transition of CPNT1 : t01 is outbound } )) )
assume P1: dom q12 = Outbds CPNT1 ; :: thesis: ( ex t01 being transition of CPNT1 st
( t01 is outbound & q12 . t01 is not Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) ) or q12 in Funcs ((Outbds CPNT1),(union { (Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))))) where t01 is transition of CPNT1 : t01 is outbound } )) )
assume P2: for t01 being transition of CPNT1 st t01 is outbound holds
q12 . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) ; :: thesis: q12 in Funcs ((Outbds CPNT1),(union { (Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))))) where t01 is transition of CPNT1 : t01 is outbound } ))
now :: thesis: for y being object st y in rng q12 holds
y in union { (Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))))) where t01 is transition of CPNT1 : t01 is outbound }
let y be object ; :: thesis: ( y in rng q12 implies y in union { (Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))))) where t01 is transition of CPNT1 : t01 is outbound } )
assume y in rng q12 ; :: thesis: y in union { (Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))))) where t01 is transition of CPNT1 : t01 is outbound }
then consider t01 being object such that
P11: ( t01 in dom q12 & y = q12 . t01 ) by FUNCT_1:def 3;
reconsider t01 = t01 as transition of CPNT1 by P1, P11;
p12: ex x being transition of CPNT1 st
( x = t01 & x is outbound ) by P1, P11;
q12 . t01 is Function of (thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))) by P2, p12;
then P13: q12 . t01 in Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01))))) by FUNCT_2:8;
Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01))))) in { (Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))))) where t01 is transition of CPNT1 : t01 is outbound } by p12;
hence y in union { (Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))))) where t01 is transition of CPNT1 : t01 is outbound } by P11, P13, TARSKI:def 4; :: thesis: verum
end;
then rng q12 c= union { (Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))))) where t01 is transition of CPNT1 : t01 is outbound } ;
hence q12 in Funcs ((Outbds CPNT1),(union { (Funcs ((thin_cylinders ( the ColoredSet of CPNT1,(*' {t01}))),(thin_cylinders ( the ColoredSet of CPNT1,(Im (O12,t01)))))) where t01 is transition of CPNT1 : t01 is outbound } )) by FUNCT_2:def 2, P1; :: thesis: verum