let S, T be non empty RelStr ; for f being set holds
( ( f is Connection of S,T implies f is Connection of S ~ ,T ) & ( f is Connection of S ~ ,T implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S,T ~ ) & ( f is Connection of S,T ~ implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S ~ ,T ~ ) & ( f is Connection of S ~ ,T ~ implies f is Connection of S,T ) )
A1:
now for S, S1, T, T1 being RelStr st the carrier of S = the carrier of S1 & the carrier of T = the carrier of T1 holds
for a being Connection of S,T holds a is Connection of S1,T1let S,
S1,
T,
T1 be
RelStr ;
( the carrier of S = the carrier of S1 & the carrier of T = the carrier of T1 implies for a being Connection of S,T holds a is Connection of S1,T1 )assume A2:
( the
carrier of
S = the
carrier of
S1 & the
carrier of
T = the
carrier of
T1 )
;
for a being Connection of S,T holds a is Connection of S1,T1let a be
Connection of
S,
T;
a is Connection of S1,T1consider f being
Function of
S,
T,
g being
Function of
T,
S such that A3:
a = [f,g]
by WAYBEL_1:def 9;
reconsider g =
g as
Function of
T1,
S1 by A2;
reconsider f =
f as
Function of
S1,
T1 by A2;
a = [f,g]
by A3;
hence
a is
Connection of
S1,
T1
;
verum end;
( S ~ = RelStr(# the carrier of S,( the InternalRel of S ~) #) & T ~ = RelStr(# the carrier of T,( the InternalRel of T ~) #) )
;
hence
for f being set holds
( ( f is Connection of S,T implies f is Connection of S ~ ,T ) & ( f is Connection of S ~ ,T implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S,T ~ ) & ( f is Connection of S,T ~ implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S ~ ,T ~ ) & ( f is Connection of S ~ ,T ~ implies f is Connection of S,T ) )
by A1; verum