let v be object ; :: thesis: for V, A being set
for f, g being SCBinominativeFunction of V,A
for x being Element of product <*g*> st v in V & product <*g*> <> {} holds
SC_Fsuperpos (f,g,v) = SC_Fsuperpos (f,x,<*v*>)
let V, A be set ; :: thesis: for f, g being SCBinominativeFunction of V,A
for x being Element of product <*g*> st v in V & product <*g*> <> {} holds
SC_Fsuperpos (f,g,v) = SC_Fsuperpos (f,x,<*v*>)
let f, g be SCBinominativeFunction of V,A; :: thesis: for x being Element of product <*g*> st v in V & product <*g*> <> {} holds
SC_Fsuperpos (f,g,v) = SC_Fsuperpos (f,x,<*v*>)
set G = <*g*>;
let x be Element of product <*g*>; :: thesis: ( v in V & product <*g*> <> {} implies SC_Fsuperpos (f,g,v) = SC_Fsuperpos (f,x,<*v*>) )
assume that
A1: v in V and
A2: product <*g*> <> {} ; :: thesis: SC_Fsuperpos (f,g,v) = SC_Fsuperpos (f,x,<*v*>)
set X = <*v*>;
set S1 = SC_Fsuperpos (f,g,v);
set S2 = SC_Fsuperpos (f,x,<*v*>);
defpred S1[ object ] means $1 in_doms <*g*>;
A3: <*g*> . 1 = g by FINSEQ_1:40;
A4: dom <*g*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
A5: dom (SC_Fsuperpos (f,g,v)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } by Def15;
SC_Fsuperpos (f,x,<*v*>) = (SCFsuperpos (<*g*>,<*v*>)) . (f,x) by A2, Def14;
then A6: dom (SC_Fsuperpos (f,x,<*v*>)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (<*g*>,<*v*>,d))) in dom f & S1[d] ) } by A2, Def13;
thus A7: dom (SC_Fsuperpos (f,g,v)) = dom (SC_Fsuperpos (f,x,<*v*>)) :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom (SC_Fsuperpos (f,g,v)) or (SC_Fsuperpos (f,g,v)) . b1 = (SC_Fsuperpos (f,x,<*v*>)) . b1 )
proof
thus dom (SC_Fsuperpos (f,g,v)) c= dom (SC_Fsuperpos (f,x,<*v*>)) :: according to XBOOLE_0:def 10 :: thesis: dom (SC_Fsuperpos (f,x,<*v*>)) c= dom (SC_Fsuperpos (f,g,v))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom (SC_Fsuperpos (f,g,v)) or a in dom (SC_Fsuperpos (f,x,<*v*>)) )
assume a in dom (SC_Fsuperpos (f,g,v)) ; :: thesis: a in dom (SC_Fsuperpos (f,x,<*v*>))
then consider d being TypeSCNominativeData of V,A such that
A8: d = a and
A9: local_overlapping (V,A,d,(g . d),v) in dom f and
A10: d in dom g by A5;
A11: S1[d]
proof
let x be object ; :: according to NOMIN_2:def 3 :: thesis: ( x in dom <*g*> implies d in dom (<*g*> . x) )
thus ( x in dom <*g*> implies d in dom (<*g*> . x) ) by A10, A3, A4, TARSKI:def 1; :: thesis: verum
end;
NDentry (<*g*>,<*v*>,d) = naming (V,A,v,(g . d)) by A1, A10, Th26;
hence a in dom (SC_Fsuperpos (f,x,<*v*>)) by A8, A9, A11, A6; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom (SC_Fsuperpos (f,x,<*v*>)) or a in dom (SC_Fsuperpos (f,g,v)) )
assume a in dom (SC_Fsuperpos (f,x,<*v*>)) ; :: thesis: a in dom (SC_Fsuperpos (f,g,v))
then consider d being TypeSCNominativeData of V,A such that
A12: a = d and
A13: global_overlapping (V,A,d,(NDentry (<*g*>,<*v*>,d))) in dom f and
A14: S1[d] by A6;
1 in dom <*g*> by A4, TARSKI:def 1;
then A15: d in dom (<*g*> . 1) by A14, Def3;
then local_overlapping (V,A,d,(g . d),v) in dom f by A1, Th26, A13, A3;
hence a in dom (SC_Fsuperpos (f,g,v)) by A5, A12, A3, A15; :: thesis: verum
end;
let a be object ; :: thesis: ( not a in dom (SC_Fsuperpos (f,g,v)) or (SC_Fsuperpos (f,g,v)) . a = (SC_Fsuperpos (f,x,<*v*>)) . a )
assume A16: a in dom (SC_Fsuperpos (f,g,v)) ; :: thesis: (SC_Fsuperpos (f,g,v)) . a = (SC_Fsuperpos (f,x,<*v*>)) . a
then consider d being TypeSCNominativeData of V,A such that
A17: d = a and
local_overlapping (V,A,d,(g . d),v) in dom f and
A18: d in dom g by A5;
NDentry (<*g*>,<*v*>,d) = naming (V,A,v,(g . d)) by A1, A18, Th26;
hence (SC_Fsuperpos (f,x,<*v*>)) . a = f . (local_overlapping (V,A,d,(g . d),v)) by A7, A16, A17, A2, Th36
.= (SC_Fsuperpos (f,g,v)) . a by A16, A17, Th37 ;
:: thesis: verum